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

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