基于串空间的安全协议形式化分析研究

doi:10.3969/j.issn.1671-1122.2020.02.005

信息网络安全 ›› 2020, Vol. 20 ›› Issue (2): 30-36.doi: 10.3969/j.issn.1671-1122.2020.02.005

基于串空间的安全协议形式化分析研究

姚萌萌¹(), 唐黎¹, 凌永兴¹, 肖卫东²

1.江南计算技术研究所,无锡 214063
2.国防大学联合勤务学院,北京 100858

收稿日期:2019-10-14 出版日期:2020-02-10 发布日期:2020-05-11
作者简介:
作者简介：姚萌萌（1982—）,男,山东,博士研究生,主要研究方向为网络安全;唐黎（1971—）,女,江苏,高级工程师,硕士,主要研究方向为信息安全;凌永兴（1965—）,男,山东,高级工程师,本科,主要研究方向为信息安全;肖卫东（1964—）,男,江苏,教授,硕士,主要研究方向为信息技术、网络安全、教育训练。
基金资助:
国家自然科学基金[91430214];核高基重大专项[2017ZX01028101]

Formal Analysis of Security Protocol Based on Strand Space

YAO Mengmeng¹(), TANG Li¹, LING Yongxing¹, XIAO Weidong²

1. Jiangnan Institute of Computing Technology, Wuxi 214063, China
2. Joint Logistics College of National Defence University of PLA, Beijing 100858, China

Received:2019-10-14 Online:2020-02-10 Published:2020-05-11

摘要/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

中图分类号:

TP309

姚萌萌, 唐黎, 凌永兴, 肖卫东. 基于串空间的安全协议形式化分析研究[J]. 信息网络安全, 2020, 20(2): 30-36.

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.

图/表 2

参考文献 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)

基于串空间的安全协议形式化分析研究

Formal Analysis of Security Protocol Based on Strand Space

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 2

参考文献 19

相关文章 15

编辑推荐

Metrics

本文评价

[1]	韩磊, 陈武平, 曾志强, 曾颖明. 区块链层级网络结构与应用研究[J]. 信息网络安全, 2020, 20(9): 112-116.
[2]	汪金苗, 谢永恒, 王国威, 李易庭. 基于属性基加密的区块链隐私保护与访问控制方法[J]. 信息网络安全, 2020, 20(9): 47-51.
[3]	边玲玉, 张琳琳, 赵楷, 石飞. 基于LightGBM的以太坊恶意账户检测方法[J]. 信息网络安全, 2020, 20(4): 73-80.
[4]	毛志来, 刘亚楠, 孙惠平, 陈钟. 区块链性能扩展与安全研究[J]. 信息网络安全, 2020, 20(3): 56-64.
[5]	郎为民, 张汉, 赵毅丰, 姚晋芳. 一种基于区块链的物联网行为监控和活动管理方案[J]. 信息网络安全, 2020, 20(2): 22-29.
[6]	周艺华, 吕竹青, 杨宇光, 侍伟敏. 基于区块链技术的数据存证管理系统[J]. 信息网络安全, 2019, 19(8): 8-14.
[7]	路爱同, 赵阔, 杨晶莹, 王峰. 区块链跨链技术研究[J]. 信息网络安全, 2019, 19(8): 83-90.
[8]	郑敏, 王虹, 刘洪, 谭冲. 区块链共识算法研究综述[J]. 信息网络安全, 2019, 19(7): 8-24.
[9]	周元健, 秦冬梅, 刘忆宁, 吕松展. 基于区块链的可信仓单系统设计[J]. 信息网络安全, 2019, 19(6): 84-90.
[10]	王文明, 施重阳, 王英豪, 危德健. 基于区块链技术的交易及其安全性研究[J]. 信息网络安全, 2019, 19(5): 1-9.
[11]	黑一鸣, 刘建伟, 张宗洋, 喻辉. 基于区块链的可公开验证分布式云存储系统[J]. 信息网络安全, 2019, 19(3): 52-60.
[12]	赵国锋, 张明聪, 周继华, 赵涛. 基于纠删码的区块链系统区块文件存储模型的研究与应用[J]. 信息网络安全, 2019, 19(2): 28-35.
[13]	王文明, 王全玉, 王英豪, 任好盼. 面向敏感区域的智能监控与预警数据库研究与设计[J]. 信息网络安全, 2019, 19(12): 1-9.
[14]	韦永霜, 陈建华, 韦永美. 基于椭圆曲线密码的RFID/NFC安全认证协议[J]. 信息网络安全, 2019, 19(12): 64-71.
[15]	吕宗平, 丁磊, 隋翯, 顾兆军. 基于时间自动机的工业控制系统网络安全风险分析[J]. 信息网络安全, 2019, 19(11): 71-81.