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

• 作者: 刘楠 王焕孝 辛丹 郑永辉 顾纯祥
• 来源期刊: 通信学报
• 学科: 工学
• 关键词: 安全协议 形式化分析 布尔可满足性 惰性分析 类型缺陷攻击
• 年，卷（期）: 2014,（11）
• 所属期刊栏目: 安全协议
• 页码范围: 117-125
• 页数: 9页
• 分类号: TN915.0
• 字数: 8071字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-436x.2014.11.013

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	顾纯祥	解放军信息工程大学网络空间安全学院	10	33	4.0	5.0
3	刘楠	解放军信息工程大学网络空间安全学院	11	90	4.0	9.0
6	郑永辉	解放军信息工程大学网络空间安全学院	8	74	4.0	8.0
8	王焕孝	解放军信息工程大学网络空间安全学院	1	2	1.0	1.0
11	辛丹	解放军信息工程大学网络空间安全学院	1	2	1.0	1.0