一种新的安全协议形式化验证方法

形式化方法能有效检验安全协议的安全性，BAN类逻辑的发展极大地促进了这一领域的研究，但是现有的BAN类逻辑仍然存在许多问题．在分析现有BAN类逻辑的基础上，提出一种新的安全协议形式化验证方法，实现现有BAN类逻辑的验证功能，并使安全协议验证工作简单可行，便于实现机器自动验证．为安全协议形式化验证提供了一种新的途径．

A New Formal Verification Method of Security Protocols

Formal verification is in effect to detect security protocols. The development of BAN-like logics promotes the research of this area. At the same time, there are many problems with current BAN-like logics. Based on analyzing these BAN-like logics, a new formal verification method of security protocols is presented. The new logic can realize verification function of current BAN-like logics, and makes the verification process implement conveniently. Consequently verification can be realized automatically. This logic gives a new approach to the formal verification of security protocols.