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

doi:10.11959/j.issn.1000-436x.2014.11.013

通信学报 ›› 2014, Vol. 35 ›› Issue (11): 117-125.doi: 10.11959/j.issn.1000-436x.2014.11.013

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

顾纯祥^1,²,王焕孝¹,郑永辉^1,²,辛丹¹,刘楠^1,²

¹ 解放军信息工程大学网络空间安全学院，河南郑州 450001
² 数学工程与先进计算国家重点实验室，江苏无锡 214125

出版日期:2014-11-25 发布日期:2017-06-20
基金资助:
河南省科技创新杰出青年基金资助项目;河南省基础与前沿技术研究基金资助项目;数学工程与先进计算国家重点实验室开放基金资助项目

SAT-based lazy formal analysis method for security protocols

Chun-xiang GU^1,²,Huan-xiao WANG¹,Yong-hui ZHENG^1,²,Dan XIN¹,Nan LIU^1,²

¹ Institute for Network Security，PLA Information Engineering University，Zhengzhou 450001，China
² State Key Laboratory of Mathematical Engineering and Advanced Computing，Wuxi 214125，China

Online:2014-11-25 Published:2017-06-20
Supported by:
Henan Provincial Science and Technology Innovation Fund for Outstanding Young;Foundation and Research in Cutting-edge Technologies in the Project of Henan Province

摘要/Abstract

摘要：

提出了一种基于布尔可满足性问题的安全协议形式化分析方法 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.

Key words: security protocols, formalization analysis, Boolean satisfiability problem, lazy analyze, type flaw attack

顾纯祥,王焕孝,郑永辉,辛丹,刘楠. 基于SAT的安全协议惰性形式化分析方法[J]. 通信学报, 2014, 35(11): 117-125.

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): 117-125.

图/表 4

表1

图1

图2

表2

参考文献 14

[1]	SUN S T ， HAWKEY K ， BEZNOSOV K . Systematically breaking and fixing OpenID security:formal analysis，semi-automated empirical evaluation，and practical countermeasures[J]. Computers & Security， 2012，31(4): 465-483.
[2]	TASSANAVIBOON A ， GONG G . OAuth and ABE based authorization in semi-trusted cloud computing:aauth[A]. Proceedings of the second international workshop on Data intensive computing in the clouds[C]. ACM， 2011. 41-50.
[3]	ARMANDO A ， COMPAGNA L . SATMC:A SAT-based model checker for security protocols[M]. Logics in Artificial Intelligence. Springer Berlin Heidelberg， 2004. 730-733.
[4]	ARMANDO A ， BASIN D ， BOICHUT Y ，et al. The AVISPA tool for the automated validation of internet security protocols and applications[A]. Computer Aided Verification[C]. Springer Berlin Heidelberg， 2005. 281-285.
[5]	BRADLEY A R . SAT-based model checking without unrolling[A]. Verification，Model Checking，and Abstract Interpretation[C]. Springer Berlin Heidelberg， 2011. 70-87.
[6]	VIZEL Y ， GRUMBERG O ， SHOHAM S . Lazy abstraction and SAT-based reachability in hardware model checking[A]. Proceedings of the 12th Conference on Formal Methods in Computer-Aided Design[C]. 2012. 173-181.
[7]	JOHNSON S ， WILSON G ， TANG Y ，et al. SATMC:A Monte Carlo Markov chain approach to SED fitting[A]. American Astronomical Society Meeting Abstracts[C]. 2013.221.
[8]	LOWE G . An attack on the Needham-Schroeder public-key authentication protocol[J]. Information Processing Letters， 1995，56(3): 131-133.
[9]	ZORN G . Microsoft PPP CHAP extensions，version 2[EB/OL]. . 2000
[10]	BIRRELL A D ， NELSON B J . Implementing remote procedure calls[J]. ACM Transactions on Computer Systems-TOCS， 1984，2(1): 39-59.
[11]	HAMMER-LAHAV D E ， HARDT D.The OAuth2 . 0 Authorization Protocol[R]. IETF Internet Draft， 2011.
[12]	HEATHER J ， LOWE G ， SCHNEIDER S . How to prevent type flaw attacks on security protocols[J]. Journal of Computer Security， 2003，11(2): 217-244.
[13]	DOLEV D ， YAO A C . On the security of public key protocols[A]. Proceedings of the IEEE 22nd Annual Symposium on Foundations of Computer Science[C]. Nashville，TN， 1981, 350-357.
[14]	DAWS C ， OLIVERO A ， TRIPAKIS S ，et al. The Tool KRONOS[M]. Springer Berlin Heidelberg， 1996. 208-219.

符号	定义
A→B :Message	实体A向实体B发送消息Message
{Message}_K	使用密钥K加密消息Message
{Message1.Message2}	Message1与Message2连接
new()	生成一个具有随机性的变量值
cons (k，S)	将变量k放入集合S中
in (k，S)	从集合 S 中按堆栈的顺序取出一个元素并赋值给k
delete (k，S)	将k从集合S中删除
ik (m)	攻击者知道消息m
msg (j，s，r，m)	在协议的第j步，实体s向实体r发送了消息m
secret(m，[s₁，…，s_i])	消息m在实体[s₁，…，s_i]之间秘密保存
witness (s，r，o，m)	实体s将变量o赋值为m，并请求与实体r认证
request (r，s，o，m，c)	在会话c中，实体r接收变量o的值为m并实现与s的认证

协议	检测状态/个	发现攻击路径	时间消耗/s
Otway-Rees	71/11	N/TFA	0.56/0.22
NSPK^[8]	21/8	MITM/MITM	0.31/0.14
CHAPv2^[9]	547/125	N/N	1.78/0.92
RPC^[10]	13/11	N/TFA	0.29/0.25
OAuth2.0^[11]	12214/8562	N/M	4.53/3.13

[1]	龚翔, 冯涛, 杜谨泽. 基于CPN的安全协议形式化建模及安全分析方法[J]. 通信学报, 2021, 42(9): 240-253.
[2]	朱辉,武衡,赵海强,赵玉清,李晖. 适用于双层卫星网络的星间组网认证方案[J]. 通信学报, 2019, 40(3): 1-9.
[3]	孟博,何旭东,张金丽,尧利利,鲁金钿. 基于计算模型的安全协议Swift语言实施安全性分析[J]. 通信学报, 2018, 39(9): 178-190.
[4]	谷文,韩继红,袁霖. SSMCI：以攻击者为中心的安全协议验证机制[J]. 通信学报, 2017, 38(10): 175-188.
[5]	杨京,范丹,张玉清. 改进的安全协议自适应分析算法[J]. 通信学报, 2015, 36(Z1): 266-276.
[6]	李永凯,刘树波,杨召唤,刘梦君. 机会网络中用户属性隐私安全的高效协作者资料匹配协议[J]. 通信学报, 2015, 36(12): 163-171.
[7]	朱玉娜，韩继红，袁霖，陈韩托，范钰丹. 基于主体行为的多方安全协议会话识别方法[J]. 通信学报, 2015, 36(11): 190-200.
[8]	焦政达,马建峰,孙聪,姚青松. 新的车辆远程诊断授权协议[J]. 通信学报, 2014, 35(11): 146-153.
[9]	顾纯祥，王焕孝，郑永辉，辛丹，刘楠. 基于SAT的安全协议惰性形式化分析方法[J]. 通信学报, 2014, 35(11): 13-116.
[10]	焦政达，马建峰，孙聪，姚青松. 新的车辆远程诊断授权协议[J]. 通信学报, 2014, 35(11): 17-154.
[11]	刘礼才1,2，殷丽华2，郭云川2，孙燕1,2. 基于CSP方法的移动自组织网络认证协议TAM的分析与改进[J]. 通信学报, 2013, 34(Z1): 8-66.
[12]	刘礼才,殷丽华,郭云川,孙燕. 基于CSP方法的移动自组织网络认证协议TAM的分析与改进[J]. 通信学报, 2013, 34(Z1): 58-66.
[13]	许金超,曾国荪,王伟. 基于软件水印的云平台下软件服务保护安全协议[J]. 通信学报, 2012, 33(Z2): 176-181.
[14]	韩志耕,陈耿,罗军舟. 多方不可否认协议的增广CSP建模与分析[J]. 通信学报, 2012, 33(Z2): 189-195.
[15]	鲁来凤,段新东,马建峰. Otway-Rees协议改进及形式化证明[J]. 通信学报, 2012, 33(Z1): 250-254.

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

SAT-based lazy formal analysis method for security protocols

在线阅读

PDF下载

可视化

被引次数

摘要/Abstract

引用本文

使用本文

图/表 4

参考文献 14

相关文章 15

Metrics

推荐阅读 0