基于事件的群组密钥协商协议形式化分析研究

doi:10.3969/j.issn.1671-1122.2022.05.004

信息网络安全 ›› 2022, Vol. 22 ›› Issue (5): 30-36.doi: 10.3969/j.issn.1671-1122.2022.05.004

基于事件的群组密钥协商协议形式化分析研究

沈延, 姚萌萌()

江南计算技术研究所,无锡 214063

收稿日期:2021-11-21 出版日期:2022-05-10 发布日期:2022-06-02
通讯作者: 姚萌萌 E-mail:wellstudy@163.com
作者简介:沈延（1983—）,男,山东,工程师,硕士,主要研究方向为高性能计算与信息安全|姚萌萌（1982—）,男,山东,工程师,博士,主要研究方向为高性能计算与信息安全
基金资助:
国家自然科学基金(91430214);国家自然科学基金(6732018);核高基重大专项(2017ZX01028101)

Research on Formal Analysis Based on Event of Group Key Agreement Protocol

SHEN Yan, YAO Mengmeng()

Jiangnan Institute of Computing Technology, Wuxi 214063, China

Received:2021-11-21 Online:2022-05-10 Published:2022-06-02
Contact: YAO Mengmeng E-mail:wellstudy@163.com

摘要/Abstract

摘要：

群组密钥协商协议应用于物联网、无线通信、区块链、视频会议等领域,是当前的一个研究热点。该协议的交互消息较多,且消息认证、加密所使用的密码算法也复杂,这就给密码协议的形式化描述与安全性分析带来一定的困难。文章基于串空间理论,提出了相关概念以及基于事件的形式化分析方法。该方法直观、简洁、有效,易于对复杂的密码协议进行形式化描述,并能简化密码协议的安全性分析过程。文章基于事件的形式化分析方法对簇间非对称群组密钥协商协议进行形式化描述和分析,发现该协议不能满足一致性,即不能认证参与协议交互节点的身份。通过对该协议的分析,也证明了文章所提形式化分析方法的有效性与正确性。

关键词: 群组密钥协商协议, 串空间, 形式化分析

Abstract:

Group key agreement protocol is a research hotspot in the fields of Internet of things, wireless, blockchain, video conference and so on. The group key agreement protocol contains many exchange messages, and the cryptographic algorithms used for message authentication and encryption are also complex, which brings certain difficulties to the formal description and security analysis of cryptographic protocols. Based on strand space theory, this paper proposed related concepts and event-based formal analysis methods. The method was intuitive, concise and effective, which was easy to formally describe complex cryptographic protocols, and could simplify the security analysis process of cryptographic protocols. In this paper, the event-based formal analysis method was used to formally describe and analyzed the group key agreement protocol. The analysis of the protocol also proved the validity and correctness of the formal analysis method proposed in this paper.

Key words: group key agreement protocol, strand space, formal analysis

中图分类号:

TP309

沈延, 姚萌萌. 基于事件的群组密钥协商协议形式化分析研究[J]. 信息网络安全, 2022, 22(5): 30-36.

SHEN Yan, YAO Mengmeng. Research on Formal Analysis Based on Event of Group Key Agreement Protocol[J]. Netinfo Security, 2022, 22(5): 30-36.

图/表 2

参考文献 12

[1]	ZHANG Jiani, HE Debiao, LI Li. Blockchain-Based Key Agreement Protocol for Internet of Things[J]. ZTE Technology Journal, 2018, 24(6): 27-31.
	张佳妮, 何德彪, 李莉. 基于区块链的物联网密钥协商协议[J]. 中兴通讯技术, 2018, 24(6): 27-31.
[2]	XIE Tao, TENG Jikai. Traitor Traceability of Asymmetric Group Key Agreement[J]. Communications Technology, 2019, 52(5): 1210-1213.
	谢涛, 滕济凯. 非对称群组密钥交换协议的叛逆追踪性[J]. 通信技术, 2019, 52(5): 1210-1213.
[3]	TENG Jikai, WU Chuankun. A Collusion Attack on Asymmetric Group Key Exchange[J]. Security and Communication Networks, 2015, 8(13): 2189-2193. doi: 10.1002/sec.1163 URL
[4]	ZHANG Lei, WU Qianhong, QIN Bo, et al. Identity-Based Authenticated Asymmetric Group Key Agreement Protocol[C]// Springer. Proceedings of COCOON 2010. Berlin: Springer, 2010: 510-519.
[5]	SHAN Chun, HU Kangwen, XUE Jingfeng, et al. Improved Pairing-Free Constant Round Certificateless Authenticated Group Key Agreement Protocol[J]. Journal of Tsinghua University(Science and Technology), 2017, 57(6): 581-585.
	单纯, 胡康文, 薛静锋, 等. 改进的无线性对固定轮数无证书群组密钥协商协议[J]. 清华大学学报(自然科学版), 2017, 57(6): 581-585.
[6]	ZHANG Qikun, GAN Yong, WANG Ruifang, et al. Inter-Cluster Asymmetric Group Key Agreement[J]. Journal of Computer Research and Development, 2018, 55(12): 69-81.
	张启坤, 甘勇, 王锐芳, 等. 簇间非对称群组密钥协商协议[J]. 计算机研究与发展, 2018, 55(12): 69-81.
[7]	ZHANG Zijian, ZHOU Qi, ZHANG Chuan, et al. New Low-Earth Orbit Satellites Authentication and Group Key Agreement Protocol[J]. Journal on Communications, 2018, 39(6): 146-153.
	张子剑, 周琪, 张川, 等. 新的低轨星座组网认证与群组密钥协商协议[J]. 通信学报, 2018, 39(6): 146-153.
[8]	WEI Yongshuang, CHEN Jianhua, WEI Yongmei. Security Authentication Protocol for RFID/NFC Based on Elliptic Curve Cryptography[J]. Netinfo Security, 2019, 12(12): 68-70.
	韦永霜, 陈建华, 韦永美. 基于椭圆曲线密码的RFID/NFC安全认证协议[J]. 信息网络安全, 2019, 12(12): 68-70.
[9]	YAO Mengmeng, TANG Li, LING Yongxing, et al. Formal Analysis of Security Protocol Based on Strand Space[J]. Netinfo Security, 2020, 20(1): 30-36.
	姚萌萌, 唐黎, 凌永兴, 等. 基于串空间的安全协议形式化分析研究[J]. 信息网络安全, 2020, 20(1): 30-36.
[10]	YAO Mengmeng, ZHU Ye, TANG Li. Research on Formal Analysis Method of Computational Soundness Based on Strand Space[C]// ACM. Proceeding of ICMAI 2019. New York: ACM, 2019: 141-145.
[11]	FABREGA F J T, HERZOG J C, GUTTMAN J D. Strand S&Paces: Why is a Security Protocol Correct?[C]// IEEE. Proceedings of the 1998 IEEE Symposium on Security and Privacy. New York: IEEE, 1998: 160-171.
[12]	YANG Haomiao, SUN Shixin, LI Hongwei. Research on Bilinear Diffie-Hellman Problem[J]. Journal of Sichuan University, 2006, 38(2): 137-140.
	杨浩淼, 孙世新, 李洪伟. 双线性Diffie-Hellman问题研究[J]. 四川大学学报:工程科学版, 2006, 38(2): 137-140.

基于事件的群组密钥协商协议形式化分析研究

Research on Formal Analysis Based on Event of Group Key Agreement Protocol

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 2

参考文献 12

相关文章 7

编辑推荐

Metrics

本文评价

[1]	陈凯杰, 熊焰, 黄文超, 武建双. 一种基于拜占庭容错的PoS共识协议形式化分析方法[J]. 信息网络安全, 2021, 21(8): 35-42.
[2]	姚萌萌, 唐黎, 凌永兴, 肖卫东. 基于串空间的安全协议形式化分析研究[J]. 信息网络安全, 2020, 20(2): 30-36.
[3]	韦永霜, 陈建华, 韦永美. 基于椭圆曲线密码的RFID/NFC安全认证协议[J]. 信息网络安全, 2019, 19(12): 64-71.
[4]	吕宗平, 丁磊, 隋翯, 顾兆军. 基于时间自动机的工业控制系统网络安全风险分析[J]. 信息网络安全, 2019, 19(11): 71-81.
[5]	姚萌萌, 朱正超, 刘明达. 一种改进的基于认证测试的形式化分析方法[J]. 信息网络安全, 2019, 19(1): 27-33.
[6]	余磊, 魏仕民, 江明明. 基于主体关联度的安全协议形式化分析方法[J]. 信息网络安全, 2018, 18(6): 45-51.
[7]	朱鹏飞, 张利琴, 李伟, 于华章. 交互型电子签名的形式化分析[J]. 信息网络安全, 2016, 16(9): 31-34.