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

【Abstract】 BAN (Burrows, Abadi and Needham) like logic can aid the design, analysis, and verification of cryptographic 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 cryptographic 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 cryptographic protocols.更多还原