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

摘要：

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

关键词：安全协议、形式化分析、布尔可满足性、惰性分析、类型缺陷攻击

所属期刊栏目：35

分类号：TN915.0

资助基金：河南省科技创新杰出青年基金资助项目134100510002;河南省基础与前沿技术研究基金资助项目142300410002;数学工程与先进计算国家重点实验室开放基金资助项目Henan Provincial Science and Technology Innovation Fund for Outstanding Young134100510002;Foundation and Research in Cutting-edge Technologies in the Project of Henan Province142300410002;Mathematical Engineering and Advanced Calculation State Key Laboratory Open Foundation

在线出版日期：2015-01-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：117-125