基于递归认证测试的SIP协议形式化分析

doi:10.3969/j.issn.1671-1122.2024.10.013

信息网络安全 ›› 2024, Vol. 24 ›› Issue (10): 1586-1594.doi: 10.3969/j.issn.1671-1122.2024.10.013

基于递归认证测试的SIP协议形式化分析

姚萌萌(), 王宇, 洪瑜平

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

收稿日期:2024-05-16 出版日期:2024-10-10 发布日期:2024-09-27
通讯作者: 姚萌萌, wellstudy@163.com
作者简介:姚萌萌（1982—），男，山东，工程师，博士，主要研究方向为网络安全|王宇（1973—），男，江苏，正高级工程师，硕士，主要研究方向为信息安全|洪瑜平（1996—），男，江西，工程师，主要研究方向为信息安全
基金资助:
国家重点研发计划(2022YFB4502000)

The Formal Analysis of SIP Protocol Based on the Recursive Authentication Test

YAO Mengmeng(), WANG Yu, HONG Yuping

Jiangnan Institute of Computing Technology, Wuxi 214063, China

Received:2024-05-16 Online:2024-10-10 Published:2024-09-27

摘要/Abstract

摘要：

文章以形式化分析方法证明协议安全为研究目的，以具有灵活性、开放性、可伸缩性等特性的SIP协议为研究对象，运用基于串空间理论改进的递归认证测试形式化分析方法，分析了一种BAN逻辑证明安全的SIP身份认证协商协议，发现了该协议执行过程中协议格式不准确、易受中间人攻击的缺陷，并提出了针对该协议缺陷的改进方案。结果表明，文章所提出的递归认证测试形式化分析方法比BAN逻辑更适用、更有效，同时改进方案也增强了SIP身份认证协商协议的安全性。

关键词: SIP协议, 递归认证测试, 串空间, 形式化分析方法

Abstract:

The article took the formal analysis method to prove the security protocol security as the research purpose, and took the SIP protocol with the characteristics of flexibility, openness and scalability as the research object. The article employed a formal analysis approach based on the improved recursive authentication test within the framework of strand space theory. It scrutinized a SIP authentication negotiation protocol that had been proven secure using BAN logic, revealing inaccuracies in protocol format and vulnerabilities to man-in-the-middle attacks during its execution. Subsequently, the article proposed a revised scheme tailored to address these identified deficiencies. The results indicate that the recursive authentication test formal analysis method employed in this article is more applicable and effective than BAN logic. Furthermore, the proposed improvements significantly enhance the security of the SIP authentication negotiation protocol.

Key words: SIP protocol, recursive authentication test, strand space, formal analysis methods

中图分类号:

TP309

姚萌萌, 王宇, 洪瑜平. 基于递归认证测试的SIP协议形式化分析[J]. 信息网络安全, 2024, 24(10): 1586-1594.

YAO Mengmeng, WANG Yu, HONG Yuping. The Formal Analysis of SIP Protocol Based on the Recursive Authentication Test[J]. Netinfo Security, 2024, 24(10): 1586-1594.

图/表 6

表1

图1

图2

图3

图4

表2

参考文献 23

[1]	ROSENBERGETAL J. SIP: Session Initiation Protocol[EB/OL]. (2022-07-06)[2024-04-01]. https://www.rfc-editor.org/rfc/rfc3261.
[2]	OSAMA S, YOUNES. A Hybrid Deep Learning Model for Detecting DDoS Flooding Attacks in SIP-Based Systems[J]. Computer Networks, 2024, 240: 110-146.
[3]	SANDHYA H S, WAYAN M, SELO S. Design and Implementation of Mobile Applications for Military Personnel Based on SIP (Session Initiation Protocol)[C]// IEEE. 2022 IEEE 12th Annual Computing and Communication Workshop(CCWC). New York: IEEE, 2022: 870-875.
[4]	YE Tengan, HUI Qinli, YUE Zhang, et al. Evaluating SIP-Based VoIP Communication Quality and Network Security[EB/OL]. (2023-11-03)[2024-04-01]. https://doi.org/10.1117/12.3026308.
[5]	ALI A, PASCAL L, ABDELHAFID A, et al. A Performance Evaluation of In-Memory Databases Operations in Session Initiation Protocol[J]. Network, 2022, 3(1): 1-14.
[6]	HUANG Chaoyang, CHEN Jinmu. A SIP Identity Authentication Key Agreement Protocol Based on ECC[J]. Dianzi Keji Daxue Xuebao/Journal of the University of Electronic Science and Technology of China, 2023, 52(5): 747-755.
	黄朝阳, 陈金木. 基于ECC的SIP身份认证密钥协商协议[J]. 电子科技大学学报, 2023, 52(5): 747-755.
[7]	LU Yanrong, LI Lixiang, PENG Haipeng, et al. A Secure and Efficient Mutual Authentication Scheme for Session Initiation Protocol[J]. Peer-to-Peer Networking and Applications, 2016, 9(2): 449-459.
[8]	KUMARI S, KARUPPIAH M, DAS A K, et al. Design of a Secure Anonymity-Preserving Authentication Scheme for Session Initiation Protocol Using Elliptic Curve Cryptography[J]. Journal of Ambient Intelligence and Humanized Computing, 2018, 9(3): 643-653.
[9]	ZHOU Yousheng, CHEN Xinyun. An Anonymous and Efficient ECC-Based Authentication Scheme for SIP[J]. Wireless Communications and Mobile Computing, 2020(11): 1-11.
[10]	HASSAN U M, CHAUDHRY S A, IRSHAD A, et al. An Improved SIP Authenticated Key Agreement Based on Dongqing[J]. Wireless Personal Communications, 2020, 110(4): 2087-2107.
[11]	MAHOR V K, PADMAVATHY R, CHATTERJEE S. Chebyshev Chaotic Map-Based Efficient Authentication Scheme for Secure Access of VoIP Services through SIP[J]. International Journal of Security and Networks, 2022, 17(1): 39-47.
[12]	OSAMA Y, UMAR A. Securing Session Initiation Protocol[J]. Sensors, 2022, 22(23): 9103-9110.
[13]	LU Yanrong, ZHAO Dawei. An Anonymous SIP Authenticated Key Agreement Protocol Based on Elliptic Curve Cryptography[J]. Mathematical Biosciences and Engineering, 2022, 19(1): 66-85. doi: 10.3934/mbe.2022003 pmid: 34902980
[14]	YAO Mengmeng, ZHU Zhengchao, LIU Mingda. An Improved Formal Analysis Method Based on Authentication Tests[J]. Netinfo Security, 2019, 19(1): 27-33.
	姚萌萌, 朱正超, 刘明达. 一种改进的基于认证测试的形式化分析方法[J]. 信息网络安全, 2019, 19(1): 27-33.
[15]	YAO Mengmeng, TANG Li, LING Yongxing, et al. Formal Analysis of Security Protocol Based on Strand Space[J]. Netinfo Security, 2020, 20(2): 30-36.
	姚萌萌, 唐黎, 凌永兴, 等. 基于串空间的安全协议形式化分析研究[J]. 信息网络安全, 2020, 20(2): 30-36.
[16]	WANG Jianhua, ZHANG Lan. A Formal Construction Attack Method for Detecting Type Defects[J]. Journal of Cryptologic Reseatch, 2021, 8(6): 1058-1073. doi: 10.13868/j.cnki.jcr.000496
	王建华, 张岚. 检测类型缺陷的形式化构造攻击方法[J]. 密码学报, 2021, 8(6): 1058-1073. doi: 10.13868/j.cnki.jcr.000496
[17]	GAO Shan. Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model[J]. Electronics, 2022, 11(4): 1333-1341.
[18]	SHEN Yan, YAO Mengmeng. Research on Formal Analysis Based on Event of Group Key Agreement Protocol[J]. Netinfo Security, 2022, 20(5): 30-36.
	沈延, 姚萌萌. 基于事件的群组密钥协商协议形式化分析研究[J]. 信息网络安全, 2022, 22(5): 30-36.
[19]	ZHANG Lan, HE Liangsheng, YU Bin. A Class of Combination Verification and Authentication Method for Synchronous Key Update[J]. Journal of Electronics & Information Technology, 2023, 45(12): 4509-4518.
	张岚, 何良生, 郁滨. 一类密钥同步更新的组合校验认证方法[J]. 电子与信息学报, 2023, 45(12): 4509-4518.
[20]	YANG Fan, ESCOBAR S, MEADOWS C, et al. Strand Spaces with Choice via a Process Algebra Semantics[EB/OL]. (2019-04-22)[2024-04-06]. https://arxiv.org/abs/1904.09946.
[21]	THAYER F J, HERZOG J C, GUTTMAN J D. Strand Space: Why is a Security Protocol Correct[C]// IEEE. IEEE Symposium on Security and Privacy. New York: IEEE, 1998: 160-171.
[22]	THAYER F J, HERZOG J C, GUTTMAN J D. Strand Space: Proving Security Protocols Correct[J]. Journal of Computer Security, 1999, 7(2): 191-230.
[23]	GUTTMAN J D, THAYER F J. Authentication Tests and the Structure of Bundles[J]. Theoretical Computer Science, 2002, 283(2): 333-380.

符号	含义
ID_i	i的账号
PW_i	i的口令
Kpri_U	私钥
PW_i_new	更新的口令
Kpri_x_new	更新的私钥
Kpri_S	服务器的私钥
Hash()	hash函数
R_U	随机数
realm	认证域标识
Kus	用户和服务器的协商密钥，该密钥由用户生成
Ksu	服务器和用户的协商密钥，该密钥由服务器生成
p	椭圆曲线上的一个点
P	攻击者所有可能获知的消息的集合
$\prec $_c	丛c上的偏序关系
\|\|	字符串连接运算符

基于递归认证测试的SIP协议形式化分析

The Formal Analysis of SIP Protocol Based on the Recursive Authentication Test

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 6

参考文献 23

相关文章 4

编辑推荐

Metrics

本文评价

文献[6]协议	文献[7]协议	文献[8]协议	本文改进协议
安全	安全	BAN逻辑	无
协议格式错误、中间人攻击	中间人攻击	递归认证测试	安全

[1]	沈延, 姚萌萌. 基于事件的群组密钥协商协议形式化分析研究[J]. 信息网络安全, 2022, 22(5): 30-36.
[2]	姚萌萌, 唐黎, 凌永兴, 肖卫东. 基于串空间的安全协议形式化分析研究[J]. 信息网络安全, 2020, 20(2): 30-36.
[3]	韦永霜, 陈建华, 韦永美. 基于椭圆曲线密码的RFID/NFC安全认证协议[J]. 信息网络安全, 2019, 19(12): 64-71.
[4]	姚萌萌, 朱正超, 刘明达. 一种改进的基于认证测试的形式化分析方法[J]. 信息网络安全, 2019, 19(1): 27-33.