BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的密码协议。该文介绍了 BAN逻辑的产生、成分和分析步骤 ,进而全面指出了 BAN逻辑的缺陷 ,由此而产生的改进的 BAN逻辑和现状 ,从而对 BAN类逻辑作了全面的回顾与展望 ,并得出结论 :BAN类逻辑仍然是密码协议分析和设计的主要工具 ,但理想化步骤是 BAN类逻辑的致命缺陷。指出了 BAN类逻辑研究工作的展望。这些结论对未来协议的形式化分析工作具有指导意义 BAN (Burrows, Abadi and Needham) logic helps to design, analyze, and validate cryptographic protocols in networks and distributed systems. This paper introduces the generation, composition and analysis steps of BAN logic, and then points out the defects of BAN logic and the resulting improved BAN logic and status quo, and then makes a comprehensive review and forecast of BAN logic. The conclusion: BAN logic is still the main tool for cryptographic protocol analysis and design, but the idealization step is a fatal flaw in BAN logic. It points out the prospect of BAN logic research. These conclusions are instructive for the formal analysis of future agreements