SSMCI:verification mechanism for security protocols centered on the attacker

Wen GU; Ji-hong HAN; Lin YUAN

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

您当前的位置：

首页 >

文章列表页 >

SSMCI:verification mechanism for security protocols centered on the attacker

Correspondences | 更新时间：2024-06-05

- SSMCI:verification mechanism for security protocols centered on the attacker
- Journal on Communications Vol. 38, Issue 10, Pages: 175-188(2017)
- 作者机构：
  
  解放军信息工程大学三院，河南郑州 450004
- 作者简介：
- 基金信息：
  
  The National Natural Science Foundation of China(1309018)
- DOI：10.11959/j.issn.1000-436x.2017208
  CLC： TP393.08
- Online First：2017-10，
  
  Published：25 October 2017
- 稿件说明：
移动端阅览
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.
DOI：

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. DOI： 10.11959/j.issn.1000-436x.2017208.

摘要

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

关键词

Keywords

references

GUTTMAN J D . Establishing and preserving protocol security goals [J ] . Journal of Computer Security , 2014 , 22 ( 2 ): 203 - 267 .

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 .

CREMERS C , MANW S . Operational semantics and verification of security protocols [M ] . Springer-Verlag Berlin Heidelberg , 2012 : 78 - 103 .

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 .

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 .

LUCA V . Automated security protocol analysis with the AVISPA tool [J ] . Electronic Notes in Theoretical Computer Science , 2006 , 155 : 61 - 86 .

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 .

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 .

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 .

PINAZO S S . Advanced features in protocol verification:theory,properties,and efficiency in maude-NPA [J ] . Escobar Román Santiago , 2015 .

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 .

SIMON M . Advanced automatic security protocol verification [D ] . ETH ZURICH , 2013 : 99 - 116 .

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 .

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 .

Views

1754

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Research on certificateless anonymous authentication and key agreement scheme of vehicle network based on CPN

Survey on privacy protection indoor positioning

Formal modeling and security analysis method of security protocol based on CPN

Security analysis of security protocol Swift implementations based on computational model

Adjusted automata learning algorithm for security protocol adaptive model checking

Related Author

SU Chunhua

FENG Tao

ZHENG Lu

Yanyan XU

Zhiheng WANG

Jinze DU

Tao FENG

Xiang GONG

Related Institution

School of Computer and Communication, Lanzhou University of Technology

Division of Computer Science, University of Aizu

State Key Laboratory of Information Engineering in Surveying Mapping and Remote Sensing, Wuhan University

College of Computer Science,South Central University For Nationalities

Information Security Research Center of State Key Laboratory of Integrated Services Networks,Xidian University

AI问答

⁰