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

doi:10.3969/j.issn.1671-1122.2018.06.006

Abstract

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

CLC Number:

TP309

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.

Figures/Tables 3

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