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

谷文; 韩继红; 袁霖

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

您当前的位置：

首页 >

文章列表页 >

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

学术通信 | 更新时间：2024-06-05

- SSMCI：以攻击者为中心的安全协议验证机制
- SSMCI:verification mechanism for security protocols centered on the attacker
- 通信学报 2017年38卷第10期页码：175-188
- 作者机构：
  
  解放军信息工程大学三院，河南郑州 450004
- 作者简介：
  
  [ "谷文（1992-），男，湖南耒阳人，解放军信息工程大学硕士生，主要研究方向为安全协议形式化分析与自动化验证。" ]
  [ "韩继红（1966-），女，山西定襄人，博士，解放军信息工程大学教授、博士生导师，主要研究方向为网络与信息安全、安全协议形式化分析与自动化验证。" ]
  [ "袁霖（1981-），男，河南商丘人，博士，解放军信息工程大学副教授，主要研究方向为安全协议形式化分析与自动化验证、软件可信性分析。" ]
- 基金信息：
  
  国家自然科学基金资助项目(1309018)
- DOI：10.11959/j.issn.1000-436x.2017208
  中图分类号： TP393.08
- 网络出版日期：2017-10，
  
  纸质出版日期：2017-10-25
- 稿件说明：
移动端阅览
谷文, 韩继红, 袁霖. 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.
谷文, 韩继红, 袁霖. SSMCI：以攻击者为中心的安全协议验证机制[J]. 通信学报, 2017,38(10):175-188. DOI： 10.11959/j.issn.1000-436x.2017208.

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 .

浏览量

861

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于CPN的车载网络无证书匿名认证和密钥协商方案研究

室内定位隐私保护综述

基于CPN的安全协议形式化建模及安全分析方法

基于计算模型的安全协议Swift语言实施安全性分析

改进的安全协议自适应分析算法