SSMCI：以攻击者为中心的安全协议验证机制

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

通信学报 ›› 2017, Vol. 38 ›› Issue (10): 175-188.doi: 10.11959/j.issn.1000-436x.2017208

• 学术通信 • 上一篇

SSMCI：以攻击者为中心的安全协议验证机制

谷文,韩继红,袁霖

解放军信息工程大学三院，河南郑州 450004

修回日期:2017-06-06 出版日期:2017-10-01 发布日期:2017-11-16
作者简介:谷文（1992-），男，湖南耒阳人，解放军信息工程大学硕士生，主要研究方向为安全协议形式化分析与自动化验证。|韩继红（1966-），女，山西定襄人，博士，解放军信息工程大学教授、博士生导师，主要研究方向为网络与信息安全、安全协议形式化分析与自动化验证。|袁霖（1981-），男，河南商丘人，博士，解放军信息工程大学副教授，主要研究方向为安全协议形式化分析与自动化验证、软件可信性分析。
基金资助:
国家自然科学基金资助项目(1309018)

SSMCI:verification mechanism for security protocols centered on the attacker

Wen GU,Ji-hong HAN,Lin YUAN

The Third College,PLA Information Engineering University,Zhengzhou 450004,China

Revised:2017-06-06 Online:2017-10-01 Published:2017-11-16
Supported by:
The National Natural Science Foundation of China(1309018)

摘要/Abstract

摘要：

提出一种能对安全协议进行分析的自动化验证机制。提出需求的概念，认为需求是攻击者未知但又对攻击者合成目标项至关重要的知识集合，并建立了以需求为中心的攻击者模型；设计一种以攻击者为中心的状态搜索方式，按需添加协议会话实例，为避免新增协议会话实例引起攻击者推理出现时序矛盾，引入回溯机制以确保状态转移过程中攻击者知识能正确增长。实验表明，该系统能正确验证协议的安全性，状态空间数目略优于Scyther工具。

关键词: 安全协议, 攻击者模型, 状态扩展

Abstract:

A automatic verification mechanism for security protocols analysis was proposed.The attacker model was proposed and the concept of ‘need’ was defined,a knowledge set which was necessary for the attacker to compose a target message term but unknown to the attacker.The attacker model was established as needed.The mechanism centered on the attacker was designed,in which whether add a protocol session was determined by the attacker.This might cause contradiction in time sequence,so some back-track algorithm was adopted to solve this contradiction.Experiments show that the system can verify the security of the protocol,and the number of state space is slightly better than the Scyther tool.

Key words: security protocol, attacker model, state expansion

中图分类号:

TP393.08

谷文,韩继红,袁霖. SSMCI：以攻击者为中心的安全协议验证机制[J]. 通信学报, 2017, 38(10): 175-188.

Wen GU,Ji-hong HAN,Lin YUAN. SSMCI:verification mechanism for security protocols centered on the attacker[J]. Journal on Communications, 2017, 38(10): 175-188.

图/表 3

图1

表1

需求实例接收消息和对应的addTermAtK(t)"

消息项	实例化	addTerm_AtK (t)
$(X \| \| a g e n t_{1}) p u b k (a g e n t_{2})$	$a g e n t_{2} / I$	X
$(X \| \| a g e n t_{1}) p u b k (a g e n t_{2})$	$a g e n t_{2} / I$	$(X \| \| a g e n t_{1}) p u b k (a g e n t_{2})$
$(X \| \| Y) p u b k (a g e n t_{1})$	$a g e n t_{1} / I$	{X,Y}
$(X \| \| Y) p u b k (a g e n t_{1})$	$a g e n t_{1} / I$	$(X \| \| Y) p u b k (a g e n t_{1})$
$(Y) p u b k (a g e n t_{1})$	$a g e n t_{1} / I$	Y
$(Y) p u b k (a g e n t_{1})$	$a g e n t_{1} / I$	$(Y) p u b k (a g e n t_{1})$

表1

表2

参考文献 15

[1]	GUTTMAN J D . Establishing and preserving protocol security goals[J]. Journal of Computer Security, 2014,22(2): 203-267.
[2]	ARMANDO A , CARBONE R , COMPAGNA L . SATMC:a SAT-based model checker for security protocols,business processes,and security APIs[J]. International Journal on Software Tools for Technology Transfer, 2016,18(2): 187-204.
[3]	CREMERS C , MANW S . Operational semantics and verification of security protocols[M]. Springer-Verlag Berlin Heidelberg, 2012: 78-103.
[4]	CREMERS C , LAFOURCADE P , NADEAU P . Comparing state spaces in automatic security protocol analysis[M]. Formal to Practical Security. Springer Berlin Heidelberg, 2009: 70-94.
[5]	DAIVD B , SEBASTIAN M , LUCA V . OFMC:a symbolic model checker for security protocols[J]. International Journal of Information Security, 2005,4(3): 181-208.
[6]	ARMANDO A , CARBONE R , COMPAGNA L . SATMC:a SAT-based model checker for security protocols,business processes,and security APIs[J]. International Journal on Software Tools for Technology Transfer, 2016,18(2): 187-204.
[7]	LUCA V . Automated security protocol analysis with the AVISPA tool[J]. Electronic Notes in Theoretical Computer Science, 2006,155: 61-86.
[8]	CHEVAL V , CORTIER V . Timing attacks in security protocols:symbolic framework and proof techniques[M]// Principles of Security and Trust,Springer Berlin Heidelberg, 2015: 280-299.
[9]	STYLIANOS B , PANAGIOTIS K , ANDREW P . An intruder model with message inspection for model checking security protocols[J]. Computers ＆ Security, 2010,29(1): 16-34.
[10]	BLANCHET B . Automatic verification of security protocols in the symbolic model:the verifier proverif[M]. Foundations of Security Analysis and Design VII. Springer International Publishing,2014, 8604: 54-87.
[11]	PINAZO S S . Advanced features in protocol verification:theory,properties,and efficiency in maude-NPA[J]. Escobar Román Santiago, 2015.
[12]	CHOTHIA T , SMYTH B , STAITE C . Automatically checking commitment protocols in ProVerif without false attacks[C]// International Conference on Principles of Security and Trust.Springer Berlin Heidelberg. 2015: 137-155.
[13]	SIMON M . Advanced automatic security protocol verification[D]. ETH ZURICH, 2013: 99-116.
[14]	MEIER S , SCHMIDT B , CREMERS C . The TAMRIN prover for the symbolic analysis of security protocols[C]// The 25th International Conference on Computer Aided Verification (CAV'13). 2013: 696-701.
[15]	BASIN D , CREMERS C . Modeling and analyzing security in the presence of compromising adversaries[C]// The 15th European Conference on Research in Computer Security,Dimitris Gritzalis,2010, 6345: 340-356.

协议名称	结果	中间状态数	可实现状态数	Scyther可实现状态数	验证时间/s
NSPK	攻击	175	2	4	0.87
NSPK-FIX	安全	101	1	1	0.55
Andrew	攻击	165	2	2	0.83
EKE	攻击	183	2	2	0.93
CHAPv2	安全	81	2	2	0.43
Helsiniki	攻击	168	2	4	0.83
Cham-MD5	安全	155	2	2	0.81

SSMCI：以攻击者为中心的安全协议验证机制

SSMCI:verification mechanism for security protocols centered on the attacker

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 3

参考文献 15

相关文章 15

Metrics

推荐阅读 0

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