Formal Analysis of Security Protocol Based on Strand Space

doi:10.3969/j.issn.1671-1122.2020.02.005

Abstract

Abstract:

Security protocols are an important component in the field of information security. With the rapid development of emerging technologies, security protocols have become more and more complex, posing a challenge to the formal analysis of security protocols. In recent years, the formal analysis method based on the strand space theory is a hot spot, and it has received attention and research in the field of security protocol analysis, and has achieved certain results. This paper extends the theory of strand space, the concepts of matching strings, matching nodes, and the same execution cluster are proposed , and formalizes the fair multi-party non-repudiation protocol based on block chain using extend strand space theory, and finds the defect the protocol can’t satisfy fairness.

Key words: strand space, formal analysis, security protocol, block chain

CLC Number:

TP309

YAO Mengmeng, TANG Li, LING Yongxing, XIAO Weidong. Formal Analysis of Security Protocol Based on Strand Space[J]. Netinfo Security, 2020, 20(2): 30-36.

Figures/Tables 2

References 19

[1]	ZHANG Wenzheng.Design and Analysis of Security Protocols[M]. Beijing: National Defense Industry Press, 2015.
	张文政. 安全协议设计与分析[M].北京:国防工业出版社,2015.
[2]	WANG Zhen, FAN Jia, CHENG Lin, et al.Supervised Anonymous Authentication Scheme[J]. Journal of Software, 2019, 30(6): 1705-1720.
	王震,范佳,成林,等.可监管匿名认证方案[J]. 软件学报,2019,30(6):1705-1720.
[3]	YUAN Boao, LIU Jun, LI Ge.Fair Multi-party Non-repudiation Protocol Based on Block Chain[J]. Journal of Cryptologic Reseatch, 2018, 5(5): 96-105.
	苑博奥,刘军,李戈.基于区块链的公平多方不可否认协议[J]. 密码学报,2018,5(5):96-105.
[4]	NORTA A, MATULEVIČIUS R, LEIDING B. Safeguarding A Formalized Blockchain-enabled Identity-authentication Protocol by Applying Security Risk-oriented Patterns[EB/OL]. , 2019-6-12.
[5]	ZHANG Xiaohan.Research on Identity Authentication Protocol of Internet of Things Equipment Based on Blockchain[D]. Hefei: University of Science and Technology of China, 2019.
	张霄涵. 基于区块链的物联网设备身份认证协议研究[D].合肥:中国科学技术大学,2019.
[6]	LI Qiang SHU Zhanxiang YU Xiang, et al. Authentication Mechanism in Blockchain Systems[J]. Journal of Command and Control, 2019, 5(1): 1-17.
	李强,舒展翔,余祥,等.区块链系统的认证机制研究[J]. 指挥与控制学报,2019,5(1):1-17.
[7]	FABREGA F J T, HERZOG J C, GUTTMAN J D. Strand S&Paces:Why is a Security Protocol Correct?[EB/OL]. , 2019-6-14.
[8]	LI Qian, WANG Zheng, MA Jianfen, et al.Lightweight Mobile Payment Protocol Fairness Analysis[J]. Computer Engineering and Applications, 2018, 54(19): 88-93.
	李茜,王峥,马建芬,等.轻量级移动支付协议公平性分析[J]. 计算机工程与应用,2018,54(19):88-93.
[9]	XIAO Yuelei, WU Junsheng, ZHU Zhixiang.Extended Internet Key Exchange Protocol Version 2 in Trusted Computing Environment[J]. Microelectronics & Computer, 2018, 35(12): 7-13.
	肖跃雷,武君胜,朱志祥.可信计算环境下的IKEv2协议扩展方案[J]. 微电子学与计算机,2018,35(12):7-13.
[10]	XIAO Yuelei, WU Junsheng, ZHU Zhixiang.Improvement and Analysis of LAN Security Association Scheme Based on Pre-shared Key[J]. Journal of Computer Applications, 2018, 38(11): 200-205.
	肖跃雷,武君胜,朱志祥.基于预共享密钥的LAN安全关联方案改进与分析[J]. 计算机应用,2018,38(11):200-205.
[11]	SONG Weitao, HU Bin.One Strong Authentication Test Suitable for Analysis of Nested Encryption Protocols[J]. Computer Science, 2015, 42(1): 149-169.
	宋巍涛,胡斌.一种适用于嵌套加密协议分析的强认证测试方法[J]. 计算机科学,2015,42(1):149-169.
[12]	MUHAMMAD S.Applying Authentication Tests to Discover Man-in-the-middle Attack in Security Protocols[C]//IEEE. 8th International Conference on Digital Information Management, September 10-12, 2013, Islamabad, Pakistan. New Jersey: IEEE, 2013: 35-40.
[13]	WEI Hao, XIE Zhenglong, YI Gaizhen.Analysis of Kerberos Protocol Based on Strand Space Theory[J]. Computer Technology and Development, 2013(12): 109-112.
	魏浩,解争龙,弋改珍.基于串空间理论的Kerberos协议分析[J]. 计算机技术与发展, 2013(12):109-112.
[14]	FENG Wei FENG Dengguo. Analyzing Trusted Computing Protocol Based on the Strand Spaces Model[J]. Chinese Journal of Computers, 2015, 38(4): 701-716.
	冯伟,冯登国.基于串空间的可信计算协议分析[J]. 计算机学报,2015,38(4):701-716.
[15]	SONG Weitao, HU Bin.Approach to Detecting Type-flaw Attacks Based on Extended Strand Spaces[J]. Computer Journal, 2018, 58(4): 572-587.
[16]	DOLEV D, YAO A.On the Security of Public Key Protocols[J]. Information Theory IEEE Transactions on, 1981, 29(2): 198-208.
[17]	FABREGA F JT, HERZOG J C, GUTTMAN J D.Strand Space: Proving Security Protocols Correct[J]. Journal of Computer Security, 1999, 7(2-3): 191-230.
[18]	GUTTMAN J D, THAYER F J.Authentication Tests and the Structure of Bundles[J]. Theoretical Computer Science, 2002, 283(2): 333-380.
[19]	YUAN Yong, WANG Feiyue.Blockchain: The State of the Art and Future Trends[J]. Acta Automatica Sinica, 2016, 42(4): 481-494.
	袁勇,王飞跃.区块链技术发展现状与展望[J]. 自动化学报,2016,42(4):481-494.

符号	意义
hmac(m,k)	表示用密钥k对m进行HMAC操作
sign_A(*)	表示用A的私钥对消息*签名
Proof_S	表示发送方的不可否认证据
Proof_R	表示接收方的不可否认证据
Proof_C	公布密钥证据
TRADING	表示A广播的交易
B,B_i	B表示主体集合,B_i表示集合中第i个元素
{k}_Bi	表示主体B_i对密钥k加密的密文消息
Con_K	表示sign_A(Proof_C,A,B_i,hmac{m,k},{k}_Bi)