SAP-AKA二次认证协议的形式化验证与改进

doi:10.19678/j.issn.1000-3428.0069175

摘要/Abstract

摘要：

SAP-AKA协议是根据第3代合作项目(3GPP)标准定义的基于可扩展身份认证(EAP)框架, 为垂直用户提供密钥服务安全的二次认证协议，在5G实际环境中，认证与密钥协商协议受到各种网络攻击的影响，导致非法访问、无法认证以及身份信息泄露，在面临巨大安全挑战下SAP-AKA协议的安全属性能否满足要求仍未知。为此, 采用概率模型检测方法对SAP-AKA协议建立形式化模型，在协议交互状态迁移中引入攻击率，定量分析攻击率对协议的影响程度，使用概率计算树逻辑描述协议属性，并利用概率模型检测工具PRISM对协议的安全属性进行定量形式化分析。实验结果表明，SAP-AKA协议的时延性、认证性和完整性在不同程度上受各实体间攻击率的影响，随着攻击率变大，协议的安全属性不再满足要求。最后根据实验结果分析造成安全缺陷的原因，提出了改进方案并进行形式化验证，协议的安全属性均得到有效提升。

关键词: 概率模型检测, 认证协议, SAP-AKA协议, 形式化验证, PRISM工具

Abstract:

The SAP-AKA protocol is a secondary authentication protocol that provides key service security for vertical users, based on the Extensible Authentication Protocol (EAP) framework defined by the 3rd Generation Partnership Project(3GPP)standard. In an actual 5G environment, authentication and key negotiation protocols are subject to various network attacks, resulting in illegal access, authentication failure, and identity information leakage. It is uncertain whether the security attributes of the SAP-AKA protocol meet the requirements under major security challenges. This study establishes a formal model of the SAP-AKA protocol using a probabilistic model checking method. The attack rate is introduced during the protocol interaction state transition to quantitatively analyze the degree of impact of the attack rate on the protocol. The protocol properties are described using probabilistic computation tree logic, and the security properties of the protocol are subjected to a quantitative formal analysis using the PRISM probabilistic model-checking tool. The experimental results show that the timeliness, authentication, and integrity of the SAP-AKA protocol are affected by the attack rate among different entities to varying degrees, and the security attributes of the protocol no longer meet the requirements as the attack rate increases. Finally, based on the experimental results, the causes of security defects are analyzed, and an improvement scheme is proposed and formalized. The security attributes of the protocol are effectively improved.

Key words: probabilistic model checking, authentication protocol, SAP-AKA protocol, formal verification, PRISM tool

彭程炜, 杨晋吉, 杨光. SAP-AKA二次认证协议的形式化验证与改进[J]. 计算机工程, 2025, 51(6): 204-211.

PENG Chengwei, YANG Jinji, YANG Guang. Formal Verification and Improvement of SAP-AKA Secondary Authentication Protocol[J]. Computer Engineering, 2025, 51(6): 204-211.

https://www.ecice06.com/CN/Y2025/V51/I6/204

图/表 16

图1 5G安全架构

Fig.1 5G security architecture

图2 二次认证问题定义

Fig.2 Definition of secondary authentication problem

图3 SAP-AKA认证流程

Fig.3 Certification procedure of SAP-AKA

图4 离散时间马尔可夫链实例图

Fig.4 Example diagram of discrete-time Markov chain

图5 时延性概率与attackSM和attackES的变化关系

Fig.5 The variation relationship between latency probability with attackSM and attackES

图6 时延性概率与attackES/attackEM的变化关系

Fig.6 The variation relationship between latency probability with attackES/attackEM

图7 时延性概率与attackES和attackEM的变化关系

Fig.7 The variation relationship between latency probability with attackES and attackEM

图8 认证性概率与attackES的变化关系

Fig.8 The variation relationship between authentication probability with attackES

图9 认证性概率与attackES/attackEM的变化关系

Fig.9 The variation relationship between authentication probability with attackES/attackEM

图10 完整性概率分别与attackES/attackSM的变化关系

Fig.10 The variation relationship between integrity probability with attackES/attackSM

图11 SAP-AKA协议改进流程

Fig.11 Improvement procedure of the SAP-AKA protocol

图12 时延性分析

Fig.12 Latency analysis

图13 认证性分析

Fig.13 Authentication analysis

图14 完整性分析

Fig.14 Integrity analysis

参考文献 25

1	JOSE L O, PABLO A, DIEGO L, et al. Network slicing for 5G with SDN/NFV: concepts, architectures, and challenges[EB/OL]. [2023-12-03]. https://arxiv.org/ftp/arxiv/papers/1703/1703.04676.pdf.
2	LUBNA N, AWAIS M A, YASAR A, et al. Integration of D2D, network slicing, and MEC in 5G cellular network: survey and challenges. IEEE Access, 2021, 9, 37590- 37612. doi: 10.1109/ACCESS.2021.3063104
3	DAIFALLAH A. Survey on network slice isolation in 5G networks: fundamental challenges. Procedia Computer Science, 2021, 182, 38- 45. doi: 10.1016/j.procs.2021.02.006
4	HEGDE P, MEENA S M. A survey on 5G network slicing-epitome and opportunities for a novice[C]//Proceedings of International Conference on Computing Communication and Networking Technologies (ICCCNT). Washington D. C., USA: IEEE Press, 2021: 1-5. URL
5	European Telecommunications Standards Institute. Security architecture and procedures for 5G system (3GPP TS 33.501 version 15.4.0. Release 15)[S/OL]. [2023-12-03]. https://www.etsi.org/deliver/etsi_ts/133500_133599/133501/15.01.00_60/ts_133501v150100p.pdf.
6	ABOBA B, BLUNK L, VOLLBRECHT J, et al. RFC 3784, Extensible Authentication Protocol (EAP)[S/OL]. [2023-12-03]. http://www.nic.funet.fi/rfc/rfc3748.txt.pdf.
7	SIMON D, ABOBA B, HURST R. The EAP-TLS authentication protocol[EB/OL]. [2023-12-03]. https://docbox.etsi.org/reference/IETF/RFC/RFC5216.pdf.
8	ARKKO J, HAVERINEN H. Extensible authentication protocol method for 3rd generation authentication and key agreement (EAP-AKA)[EB/OL]. [2023-12-03]. https://docbox.etsi.org/reference/IETF/RFC/RFC4187.pdf.
9	ARKKO J, LEHTOVIRTA V, ERONEN P. Improved extensible authentication protocol method for 3rd generation authentication and key agreement (EAP-AKA')[EB/OL]. [2023-12-03]. https://core.ac.uk/download/pdf/24065645.pdf.
10	马媛媛, 李尼格, 邵志鹏, 等. 适用于电力5G终端的二次认证方法及其形式化分析. 自动化与仪表, 2022, 37(11): 103- 108. doi: 10.19557/j.cnki.1001-9944.2022.11.021
	MA Y Y, LI N G, SHAO Z P, et al. Secondary authentication method suitable for power 5G terminal and its formal analysis. Automation & Instrumentation, 2022, 37(11): 103- 108. doi: 10.19557/j.cnki.1001-9944.2022.11.021
11	HAO Q F, SUN L, GUO S H, et al. 5G secondary authentication based on EAP-TLS protocol[C]//Proceedings of International Conference on Computer Technology and Media Convergence Design (CTMCD). Washington D. C., USA: IEEE Press, 2021: 296-300. URL
12	李长隆, 古毅, 王俊. 5G二次认证协议的分析与设计. 通信技术, 2019, 52(7): 1733- 1739. doi: 10.3969/j.issn.1002-0802.2019.07.033
	LI C L, GU Y, WANG J. Analysis and design of secondary authentication protocol in 5G. Communication Technology, 2019, 52(7): 1733- 1739. doi: 10.3969/j.issn.1002-0802.2019.07.033
13	GONG S, EL AZZAOUI A, CHA J, et al. Secure secondary authentication framework for efficient mutual authentication on a 5G data network. Applied Sciences, 2020, 10(2): 727. doi: 10.3390/app10020727
14	EDRIS E K K, AIASH M, LOO J K K. Network service federated identity (NS-FId) protocol for service authorization in 5G network[C]//Proceedings of the 15th International Conference on Fog and Mobile Edge Computing (FMEC). Washington D. C., USA: IEEE Press, 2020: 128-135. URL
15	EDRIS K K E, AIASH M, LOO K K J. Formal veritication of secondary authentication potocol for 5G secondary authentication. International Journal of Security and Networks, 2021, 16(4): 223- 234. doi: 10.1504/IJSN.2021.119379
16	LI X H, LIU H, WEI F S, et al. A lightweight anonymous authentication protocol using k-pseudonym set in wireless networks[C]//Proceedings of 2015 IEEE Global Communications Conference. Washington D. C., USA: IEEE Press, 2015: 113-120. URL
17	BASIN D, DREIER J, HIRSCHI L, et al. A formal analysis of 5G authentication[EB/OL]. [2023-12-03]. https://arxiv.org/pdf/1806.10360.
18	CREMERS C J F, DEHNEL-WILD M. Component-based formal analysis of 5G-AKA: channel assumptions and session confusion[C]//Proceedings of Conference on Network and Distributed System Security Symposium (NDSS). [S. l. ]: AAAI Press, 2019: 23-31. URL
19	刘彩霞, 胡鑫鑫, 刘树新, 等. 基于Lowe分类法的5G网络EAP-AKA'协议安全性分析. 电子与信息学报, 2019, 41(8): 1800- 1807. doi: 10.11999/JEIT190063
	LIU C X, HU X X, LIU S X, et al. Security analysis of 5G network EAP-AKA' protocol based on Lowe's taxonomy. Journal of Electronics and Information, 2019, 41(8): 1800- 1807. doi: 10.11999/JEIT190063
20	KWIATKOWSKA M, NORMAN G, PARKER D. Advances and challenges of probabilistic model checking[C]//Proceedings of Conference on Communication, Control, and Computing. Washington D.C., USA: IEEE Press, 2010: 1691-1698. URL
21	KWIATKOWSKA M, NORMAN G, PARKER D. PRISM 4.0: verification of probabilistic real-time systems[C]//Proceedings of the 23rd International Conference on Computer Aided Verification. Berlin, Germany: Springer, 2011: 585-591.
22	KWIATKOWSKA M, NORMAN G, PARKER D. Probabilistic model checking: advances and applications[M]//DRECHSLER R, Formal system verification: state-of the-art and future trends. Berlin, Germany: Springer, 2017: 73-121.
23	HINTON A, KWIATKOWSKA M, NORMAN G, et al. PRISM: a tool for automatic verification of probabilistic systems[C]//Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Germany: Springer, 2006: 441-444. URL
24	SONG S Z, GUI L, SUN J, et al. Improved reachability analysis in DTMC via divide and conquer[C]//Proceedings of the 10th International Conference on Integrated Formal Methods. Berlin, Germany: Springer, 2013: 162-176. URL
25	LIU Y, LI X D, MA Y. A game-based approach for PCTL *stochastic model checking with evidence. Journal of Computer Science and Technology, 2016, 31, 198- 216. doi: 10.1007/s11390-016-1621-y

[1]	王湛, 张鹏程, 金惠颖, 吉顺慧. 云网融合环境下服务组合的未来属性验证[J]. 计算机工程, 2025, 51(3): 310-319.
[2]	王文斌, 钱振江, 靳勇, 孙高飞, 邢晓双, 苏超, 孙天琦. 基于Isabelle/HOL的文件系统形式化设计与验证[J]. 计算机工程, 2024, 50(4): 277-285.
[3]	夏锐, 钱振江, 刘苇. 一种基于Isabelle/HOL的安全通信协议验证方法[J]. 计算机工程, 2021, 47(1): 146-153.
[4]	欧阳恒一, 熊焰, 黄文超. 一种代币智能合约的形式化建模与验证方法[J]. 计算机工程, 2020, 46(10): 41-45,51.
[5]	刘博雅,张悦,杨亚涛,孙亚飞. 基于PUF函数的轻量级双向认证协议[J]. 计算机工程, 2019, 45(2): 38-41,52.
[6]	卿哲嘉. 基于LPN具有一般中间人安全的两轮认证协议[J]. 计算机工程, 2019, 45(2): 129-133.
[7]	祁龙云, 吕小亮, 路红, 黄皓. 汇编级顺序语句块的自动形式化规约及其验证[J]. 计算机工程, 2019, 45(10): 64-69,77.
[8]	林荣峰, 施健, 朱晏庆, 沈怡颹, 周宇. 基于STP方法的SCADE模型形式化验证框架[J]. 计算机工程, 2019, 45(10): 70-77.
[9]	曾艾婧,文捷,刘百祥. 基于LPN的抗擦除攻击认证协议[J]. 计算机工程, 2019, 45(1): 141-144,152.
[10]	万爱兰,韩牟,马世典,王运文,华蕾,冯晓林. 基于一次性密码本的车内网身份认证协议[J]. 计算机工程, 2018, 44(6): 141-146,161.
[11]	李堃,张雪松. STP安全通信协议设计与形式化验证[J]. 计算机工程, 2018, 44(12): 120-128.
[12]	彭彦彬,田野,彭新光. 一种端到端的医疗无线体域网轻量认证协议[J]. 计算机工程, 2017, 43(6): 73-77.
[13]	李子臣,刘博雅,王培东,杨亚涛. 基于SM2与零知识的射频识别双向认证协议[J]. 计算机工程, 2017, 43(6): 97-100,104.
[14]	李青,朱晓冉,郭建. AUTOSAR OS存储保护机制的形式化验证框架[J]. 计算机工程, 2017, 43(1): 79-85.
[15]	刘博雅,刘年义,杨亚涛,李子臣. 基于椭圆曲线密码的无线射频识别双向认证协议[J]. 计算机工程, 2017, 43(1): 196-200.

选择文件类型/文献管理软件名称

选择包含的内容