| 基于SAT的安全协议惰性形式化分析方法 |
| |
| 引用本文： | 顾纯祥,王焕孝,郑永辉,辛 丹,刘 楠.基于SAT的安全协议惰性形式化分析方法[J].通信学报,2014,35(11):13-125. |
| |
| 作者姓名： | 顾纯祥 王焕孝 郑永辉 辛 丹 刘 楠 |
| |
| 作者单位： | 1. 解放军信息工程大学 网络空间安全学院，河南 郑州 450001；2. 数学工程与先进计算国家重点实验室，江苏 无锡 214125 |
| |
| 基金项目： | 河南省科技创新杰出青年基金资助项目（134100510002）；河南省基础与前沿技术研究基金资助项目（142300410002）；数学工程与先进计算国家重点实验室开放基金资助项目 |
| |
| 摘 要： | 提出了一种基于布尔可满足性问题的安全协议形式化分析方法SAT-LMC，通过引入惰性分析的思想优化初始状态与转换规则，提高了安全性的检测效率。另一方面，通过在消息类型上定义偏序关系，SAT-LMC能够检测出更丰富的类型缺陷攻击。基于此方法实现了一个安全协议分析工具，针对Otway-Rees协议检测出了一种类型缺陷攻击；针对OAuth2.0协议，检测结果显示对现实中存在的一些应用场景，存在一种利用授权码截取的中间人攻击。
|
| 关 键 词： | 安全协议 形式化分析 布尔可满足性 惰性分析 类型缺陷攻击 |
SAT-based lazy formal analysis method for security protocols |
| |
| Chun-xiang GU,Huan-xiao WANG,Yong-hui ZHENG,Dan XIN,Nan LIU.SAT-based lazy formal analysis method for security protocols[J].Journal on Communications,2014,35(11):13-125. |
| |
| Authors: | Chun-xiang GU Huan-xiao WANG Yong-hui ZHENG Dan XIN Nan LIU |
| |
| Affiliation: | 1. Institute for Network Security，PLA Information Engineering University，Zhengzhou 450001，China;2. State Key Laboratory of Mathematical Engineering and Advanced Computing，Wuxi 214125，China |
| |
| Abstract: | A SAT-based security protocol formalization analysis method named SAT-LMC is proposed.The method introduces optimized the initial state and transformational rules with “lazy” idea.The efficiency of detection is significantly improved.Moreover，by adding support for strong type flaw attack defect，the attack detection becomes more comprehensive.A security protocol analysis tool is implemented based on the method; a type flaw attack is detected for protocol Otway-Rees.For OAuth2.0 protocol，analysis shows that there is a kind of man-in-the-middle attack of the authorization code in some application scenarios. |
| |
| Keywords: | security protocols formalization analysis Boolean satisfiability problem lazy analyze type flaw attack |
|
| 点击此处可从《通信学报》浏览原始摘要信息 |
|
点击此处可从《通信学报》下载全文 |
