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

SAT-based lazy formal analysis method for security protocols

作　　者：顾纯祥[1,2] 王焕孝 郑永辉[1,2] 辛丹[1] 刘楠[1] 

机构地区：[1]解放军信息工程大学网络空间安全学院,河南郑州450001 [2]数学工程与先进计算国家重点实验室,江苏无锡214125

出　　处：《通信学报》2014年第11期117-125,共9页Journal on Communications

基　　金：河南省科技创新杰出青年基金资助项目(134100510002);河南省基础与前沿技术研究基金资助项目(142300410002);数学工程与先进计算国家重点实验室开放基金资助项目~~

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

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

分 类 号：TN915.0[电子电信—通信与信息系统]