基于主体关联度的安全协议形式化分析方法

doi:10.3969/j.issn.1671-1122.2018.06.006

信息网络安全 ›› 2018, Vol. 18 ›› Issue (6): 45-51.doi: 10.3969/j.issn.1671-1122.2018.06.006

基于主体关联度的安全协议形式化分析方法

余磊, 魏仕民, 江明明()

淮北师范大学计算机科学与技术学院,安徽淮北 235000

收稿日期:2018-05-08 出版日期:2018-06-15 发布日期:2020-05-11
作者简介:
作者简介：余磊（1978—）,男,安徽,副教授,硕士,主要研究方向为信息安全、安全协议;魏仕民（1962—）,男,安徽,教授,博士,主要研究方向为密码学、信息安全;江明明（1984—）,男,安徽,讲师,博士,主要研究方向为密码学、信息安全。
基金资助:
国家自然科学基金[61300048,61572224];安徽省自然科学基金[1608085MF143, 1708085QF154];安徽省高校优秀青年人才计划项目[gxyq2017154];安徽省教育厅自然科学项目[KJ2014A231,KJ2016A627]

Formal Analysis Method of Security Protocol Based on Correlation Degree of Principals

Lei YU, Shimin WEI, Mingming JIANG()

School of Computer Science and Technology, Huaibei Normal University, Huaibei Anhui 235000, China

Received:2018-05-08 Online:2018-06-15 Published:2020-05-11

摘要/Abstract

摘要：

建立在协议主体参数新近一致性上的主体关联度由于能够正确反映协议安全属性与协议结构、消息组件和消息参数的逻辑关系,因此不仅能够为安全协议的正确性分析提供准确严谨的形式化判断依据,还能进一步降低协议分析的复杂度。为此,文章提出一种基于主体关联度的安全协议形式化分析方法。该方法首先在认证测试模型上,通过对消息组件的参数分类,给出协议主体关联度的量化定义;再根据认证测试规则和测试组件上的参数一致性判定条件,建立协议关联性、认证性、协商数据一致性与协议主体关联度的逻辑关联;接着在协议主体关联度上实现对安全协议设计目标的正确性分析。文章运用该方法对Neuman-Stubblebine协议进行分析,准确发现了协议中潜在的隐患及其根源,并证实了协议主体关联度在安全协议正确性分析中的应用可行性和有效性。

关键词: 安全协议, 认证测试, 关联度, 形式化分析

Abstract:

The correlation degree of principals established on recent consistency of protocol principals parameters can correctly reflect the logical relationship between protocol security properties and protocol structure, message components and message parameters, which not only can provide accurate and rigorous formal judgment basis for the analysis of the correctness of the security protocol, but can further reduce the complexity of protocol analysis. Therefore, this paper proposes a formal analysis method for security protocols based on correlation degree of principals. Firstly, on the authentication test model, the parameters of message components are classified, and the quantitative definition of the correlation degree of the protocol principals is given. Then according to the rules of authentication test and the criteria for determining the consistency of the parameters on the components, the logical association between the correlation, authentication and the consistency of the negotiation data of the protocol and correlation degree of protocol principals is established. Next, the correctness of the design goals of security protocol is analyzed on the correlation degree of protocol principals. This paper analyzes the Neuman-Stubblebine protocol using the method, which accurately finds the potential defects and its roots in the protocol, and confirms the application feasibility and efficiency of the correlation degree of protocol principals in the correctness analysis of the security protocol.

Key words: security protocol, authentication test, correlation degree, formal analysis

中图分类号:

TP309

余磊, 魏仕民, 江明明. 基于主体关联度的安全协议形式化分析方法[J]. 信息网络安全, 2018, 18(6): 45-51.

Lei YU, Shimin WEI, Mingming JIANG. Formal Analysis Method of Security Protocol Based on Correlation Degree of Principals[J]. Netinfo Security, 2018, 18(6): 45-51.

图/表 3

参考文献 16

[1]	LI Zhicong, ZHOU Zhiping.Enhanced Secure RFID Authentication Protocol in IoT[J]. Netinfo Security, 2018,18(1):80-87.
	李智聪,周治平.物联网中增强安全的RFID认证协议[J].信息网络安全,2018,18(1):80-87.
[2]	YU Jingang, ZHAO Zhigang.Improved NSSK Authentication Protocol and its Research and Application[J]. Journal of Chinese Computer Systems,2018 (3):468-473.
	于金刚,赵治刚.一种改进的NSSK认证协议及其实现方法[J].小型微型计算机系统,2018 (3):468-473.
[3]	TANG Chunming, GAO Long.Multi-parties Key Agreement Protocol in Block Chain[J]. Netinfo Security, 2017,17(12):17-21.
	唐春明,高隆.区块链系统下的多方密钥协商协议[J].信息网络安全,2017,17(12):17-21.
[4]	KANOVICH M, KIRIGIN T B, NIGAM V, et al. Towards Timed Models for Cyber-physical Security Protocols[EB/OL]., 2018-5-3.
[5]	QU Juan, LI Yanping,LI Li.Cryptanalysis and Security Enhancement of an Efficient Secure Authentication Scheme with User Anonymity for Roaming User in Ubiquitous Networks[J].Netinfo Security,2018,1(1):73-79.
	屈娟,李艳平,李丽.普适计算中匿名跨域认证协议的分析与改进[J].信息网络安全,2018,1(1):73-79.
[6]	THAYER F J, HERZOG J C, GUTTMAN J D. Strand Spaces: Why Is a Security Protocol Correct? [EB/OL]. .
[7]	THAYER F J, HERZOG J C, GUTTMAN J D.Strand Spaces: Proving Security Protocols Correct[J]. IOS Press, 1999(2):191-230.
[8]	GUTTMAN J D, THAYER F J. Authentication Tests[EB/OL]. .
[9]	GUTTMAN J D. Security Protocol Design via Authentication Tests[EB/OL]. .
[10]	GUTTMAN J D, THAYER F J.Authentication Tests and the Structure of Bundles[J].Theoretical Computer Science, 2002(2):333-380.
[11]	LI Xiehua, YANG Shutang, LI Jianhua, et al.The Analysis Method of Authentication Tests Based on Message Type Checking[J]. Journal of Shanghai Jiaotong University, 2007(1): 85-89,99.
	李谢华,杨树堂,李建华,等.基于消息类型检测的认证测试分析方法[J].上海交通大学学报,2007(1):85-89,99.
[12]	LUO Junzhou, YANG Ming.Analysis of Security Protocols Based on Challenge-response[J]. Chinese science E: Information Science, 2006(12):1421-1441.
	罗军舟,杨明.基于挑战—响应的安全协议分析[J].中国科学E辑:信息科学,2006(12):1421-1441.
[13]	ZHOU Qinglei, WANG Feng, ZHAO Dongming.An Agreement Analysis Method of Security Protocol Based on Authentication Test[J]. Computer Science, 2007 (10):99-102.
	周清雷,王峰,赵东明.基于认证测试的一种安全协议一致性分析方法[J].计算机科学,2007(10):99-102.
[14]	YU Lei, WEI Shimin, ZHUO Zepeng.Research on Consistence of Strand Parameters for Protocol Principals in Authentication Test Theory[J]. Computer Engineering and Applications, 2015(13):86-91.
	余磊,魏仕民,卓泽朋.认证测试中协议主体串参数一致性研究[J].计算机工程与应用,2015(13):86-91.
[15]	NEUMAN B C, STUBBLEBINE S G.A Note on the Use of Timestamps as Nonces[J]. Operating Systems Review, 1993,27(2):10-14.
[16]	DING Mengwei, ZHOU Qinglei, ZHAO Dongming.The Strand Space Model of Neuman-Stubblebine Protocol and Its Analysis[J]. Computer Applications & Software, 2009 (5):37-39.
	丁萌伟,周清雷,赵东明.Neuman-Stubblebine协议的串空间模型及分析[J].计算机应用与软件,2009 (5):37-39.

基于主体关联度的安全协议形式化分析方法

Formal Analysis Method of Security Protocol Based on Correlation Degree of Principals

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 3

参考文献 16

相关文章 11

编辑推荐

Metrics

本文评价

[1]	姚萌萌, 唐黎, 凌永兴, 肖卫东. 基于串空间的安全协议形式化分析研究[J]. 信息网络安全, 2020, 20(2): 30-36.
[2]	吕宗平, 丁磊, 隋翯, 顾兆军. 基于时间自动机的工业控制系统网络安全风险分析[J]. 信息网络安全, 2019, 19(11): 71-81.
[3]	姚萌萌, 朱正超, 刘明达. 一种改进的基于认证测试的形式化分析方法[J]. 信息网络安全, 2019, 19(1): 27-33.
[4]	易辉凡, 万良, 黄娜娜, 王鹍鹏. 基于SPIN的安全协议的攻击者建模方法研究[J]. 信息网络安全, 2018, 18(2): 61-70.
[5]	朱鹏飞, 张利琴, 李伟, 于华章. 交互型电子签名的形式化分析[J]. 信息网络安全, 2016, 16(9): 31-34.
[6]	杨元原, 陆臻, 顾健. RFID安全协议追踪攻击的形式化分析[J]. 信息网络安全, 2015, 15(9): 25-28.
[7]	张蕾，郑飞. 无线局域网安全协议的分析和研究[J]. 信息网络安全, 2014, 14(9): 132-137.
[8]	刘宇靓;任伟. 基于通用可组合理论的协议安全性证明方法讨论[J]. , 2012, 12(6): 0-0.
[9]	铁玲;易勇;何迪. 多跳快速切换代理移动IPv6预认证协议的安全分析[J]. , 2012, 12(6): 0-0.
[10]	刘磊;周庆;井蔚;刘冰. 基于多核处理器的网络安全协议并行处理研究[J]. , 2011, 11(9): 0-0.
[11]	刘明华;任志考;董洪灿. 基于Web安全的电子商务安全模型研究[J]. , 2009, 9(4): 0-0.