通信学报

• 安全协议 • 上一篇    下一篇

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

顾纯祥,王焕孝,郑永辉,辛 丹,刘 楠   

  1. 1. 解放军信息工程大学 网络空间安全学院,河南 郑州 450001;2. 数学工程与先进计算国家重点实验室,江苏 无锡 214125
  • 出版日期:2014-11-25 发布日期:2014-11-15
  • 基金资助:
    河南省科技创新杰出青年基金资助项目(134100510002);河南省基础与前沿技术研究基金资助项目(142300410002);数学工程与先进计算国家重点实验室开放基金资助项目

SAT-based lazy formal analysis method for security protocols

  • Online:2014-11-25 Published:2014-11-15

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

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.

No Suggested Reading articles found!