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

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

Abstract

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

CLC Number:

TP393.08

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.

Figures/Tables 3

消息项	实例化	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})$

References 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.

Metrics

Recommended 0

No Suggested Reading articles found!

协议名称	结果	中间状态数	可实现状态数	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:verification mechanism for security protocols centered on the attacker

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 3

References 15

Related Articles 15

Metrics

Recommended 0

[1]	Xiang GONG, Tao FENG, Jinze DU. Formal modeling and security analysis method of security protocol based on CPN [J]. Journal on Communications, 2021, 42(9): 240-253.
[2]	Bo MENG,Xudong HE,Jinli ZHANG,Lili YAO,Jintian LU. Security analysis of security protocol Swift implementations based on computational model [J]. Journal on Communications, 2018, 39(9): 178-190.
[3]	Jing YANG,Dan FAN,Yu-qing ZHANG. Adjusted automata learning algorithm for security protocol adaptive model checking [J]. Journal on Communications, 2015, 36(Z1): 266-276.
[4]	. Towards session identification using principal behavior for multi-party secure protocol [J]. Journal on Communications, 2015, 36(11): 190-200.
[5]	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.
[6]	Zheng-da JIAO,Jian-feng MA,Cong SUN,Qing-song YAO. New remote authorization protocol for vehicle diagnosis [J]. Journal on Communications, 2014, 35(11): 146-153.
[7]	. SAT-based lazy formal analysis method for security protocols [J]. Journal on Communications, 2014, 35(11): 13-116.
[8]	. New remote authorization protocol for vehicle diagnosis [J]. Journal on Communications, 2014, 35(11): 17-154.
[9]	. Analysis and improvement for authentication protocols ofmobile ad hoc network with CSP approach [J]. Journal on Communications, 2013, 34(Z1): 8-66.
[10]	Rong-sen LI,Wen-hua DOU. SIM: a secure IP protocol for MANET [J]. Journal on Communications, 2013, 34(Z1): 116-125.
[11]	. SIM: a secure IP protocol for MANET [J]. Journal on Communications, 2013, 34(Z1): 15-125.
[12]	Li-cai LIU,Li-hua YIN,Yun-chuan GUO,Yan SUN. Analysis and improvement for authentication protocols of mobile ad hoc network with CSP approach [J]. Journal on Communications, 2013, 34(Z1): 58-66.
[13]	Jin-chao XU,Guo-sun ZENG,Wei WANG. Software services protection security protocol based on software watermarking in cloud environment [J]. Journal on Communications, 2012, 33(Z2): 176-181.
[14]	Lai-feng LU,Xin-dong DUAN,Jian-feng MA. Improvement and formal proof on protocol Otway-Rees [J]. Journal on Communications, 2012, 33(Z1): 250-254.
[15]	Xing-hua LI,Shuai-tuan LI,Deng LI,Jian-feng MA. Multi-language oriented automatic realization method for cryptographic protocols [J]. Journal on Communications, 2012, 33(9): 152-159.