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

BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的安全协议。介绍BAN逻辑的产生、成分和分析步骤，指出BAN逻辑的缺陷，由此而产生的改进BAN逻辑和现状，并对BAN类逻辑作全面的回顾与展望，得出：BAN类逻辑仍然是密码协议分析和设计的主要工具，但理想化步骤是BAN类逻辑的致命缺陷的结论。展望了BAN类逻辑研究。对未来协议的形式化分析工作具有指导意义。

A formal analysis method for authentication protocols

BAN(Burrows,Abadi and Needham)-like logic can aid the design,analysis,and verification of Authentication protocols used over open networks and distributed systems.This paper introduces BAN-like logic and then illustrates the limitations of BAN logic on protocol idealization as a survey of the current state of BAN-like logic.The conclusions are that BAN-like logic is still one of the main tools for analysis of authentication protocols,but protocol idealization is the fatal weakness of BAN-like logic.Suggestions are then made for future work.These conclusions will facilitate the development of formal methods for the analysis and design of authentication protocols.