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

摘要

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