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

A New Formal Verification Method of Security Protocols

作　　者：侯峻峰[1] 张磊[1] 黄连生[1] 

机构地区：[1]清华大学计算机科学与技术系网络技术研究所,北京100084

出　　处：《计算机研究与发展》2004年第8期1415-1420,共6页Journal of Computer Research and Development

摘　　要：形式化方法能有效检验安全协议的安全性 ,BAN类逻辑的发展极大地促进了这一领域的研究 ,但是现有的BAN类逻辑仍然存在许多问题 在分析现有BAN类逻辑的基础上 ,提出一种新的安全协议形式化验证方法 ,实现现有BAN类逻辑的验证功能 ,并使安全协议验证工作简单可行 ,便于实现机器自动验证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.

关 键 词：安全协议 形式化验证 BAN类逻辑 自动验证 

分 类 号：TP309.08[自动化与计算机技术—计算机系统结构]