基于SAT的安全协议惰性形式化分析方法

提出了一种基于布尔可满足性问题的安全协议形式化分析方法 SAT-LMC,通过引入惰性分析的思想优化初始状态与转换规则,提高了安全性的检测效率。另一方面,通过在消息类型上定义偏序关系,SAT-LMC 能够检测出更丰富的类型缺陷攻击。基于此方法实现了一个安全协议分析工具,针对 Otway-Rees 协议检测出了一种类型缺陷攻击;针对 OAuth2.0 协议,检测结果显示对现实中存在的一些应用场景,存在一种利用授权码截取的中间人攻击。