Abstract: Based on the Spi calculus and the logic programming rules, a new technique is presented to verify cryptographic protocols. The technique makes it possible to verify security of the protocols, in a fully automatic way. By analyzing the EKE protocol, it finds a new attack——parallel session attack, and this result demonstrates the analysis power of the technique for protocol security.

Key words: Process calculus, Logic programming, Automatic verification, Cryptographic protocols

摘要： 基于逻辑编程规则及Spi演算提出了一种验证密码协议安全性的新方法，利用该方法可以对密码协议的安全性质以程序化的方式进行验证。通过对EKE协议进行的分析，不但证明了协议已知的漏洞，而且发现了针对EKE协议的一个新的攻击——并行会话攻击。很好地验证了该新方法对密码协议的分析能力。

关键词: 进程演算, 逻辑编程, 自动验证, 密码协议