Security analysis of 5G authentication and key agreement protocol
JIA Fan1, YAN Yan2, YUAN Kaiguo3, ZHAO Lujing1
1. School of Electronic and Information Engineering, Beijing Jiaotong University, Beijing 100044, China; 2. China Cybersecurity Review Technology and Certification Center, Beijing 100020, China; 3. School of Cyberspace Security, Beijing University of Posts and Telecommunication, Beijing 100876, China
Abstract：5G networks are developing rapidly. The security of the authentication and key agreement protocols is the core issue of 5G security. The TAMARIN prover is used here to analyze the EAP-AKA' protocol for 5G networks. The protocol specifications are analyzed to identify the security requirements as a confidential attribute and an authentication attribute. A model is then established according to the TAMARIN standard to verify that these security attributes are satisfied. The verification results show a single shot consistency violation between SEAF and AUSF regarding SNID and a violation of the forward secrecy of the anchor key KSEAF, which may lead to the network experiencing replay attacks, authentication synchronization failure attacks, and Anchor key KSEAF leak attacks. Security hardening methods are then presented for these attacks with theoretical and experimental verification.
[1] 冯登国, 徐静, 兰晓. 5G移动通信网络安全研究[J]. 软件学报, 2018, 29(6):1813-1825.FENG D G, XU J, LAN X. Study on 5G mobile communication network security[J]. Journal of Software, 2018, 29(6):1813-1825.(in Chinese) [2] 邱勤, 张滨, 吕欣. 5G安全需求与标准体系研究[J]. 信息安全研究, 2020(8):673-679QIU Q, ZHANG B, LÜ X. Research on the requirements and standard system of 5G cybersecurity[J]. Journal of Information Security Research, 2020(8):673-679(in Chinese) [3] MJLSNES S F, OLIMID R F. Easy 4G/LTE IMSI catchers for nonprogrammers[C]//International Conference on Mathematical Methods, Models, and Architectures for Computer Network Security. Warsaw, Poland:Springer, 2017:235-246. [4] HUSSAIN S R, ECHEVERRIA M, CHOWDHURY O, et al. Privacy attacks to the 4G and 5G cellular paging protocols using side channel information[C]//Proceedings of the Network and Distributed System Security Symposium (NDSS). San Diego, USA, 2019:23442. [5] KIM H, LEE J, LEE E, et al. Touching the untouchables:Dynamic security analysis of the LTE control plane[C]//2019 IEEE Symposium on Security and Privacy (SP). San Francisco, USA:IEEE, 2019:1153-1168. [6] RUPPRECHT D, KOHLS K, HOLZ T and PÖPPER C. Breaking LTE on Layer Two[C]//2019 IEEE Symposium on Security and Privacy (SP). San Francisco, USA:IEEE, 2019:1121-1136. [7] HUSSAIN S R, CHOWDHURY O, MEHNAZ S, et al. LTEInspector:A systematic approach for adversarial testing of 4G LTE[C]//Proceedings of the Network and Distributed System Security Symposium. San Diego, USA:IEEE, 2018:23313. [8] ARAPINIS M, MANCINI L, RITTER E, et al. New privacy issues in mobile telephony:Fix and verification[C]//Proceedings of 2012 ACM Conference on Computer and Communications Security, Raleigh, USA, 2012:205-216. [9] 陆峰, 郑康锋, 钮心忻, 等. 3GPP认证与密钥协商协议安全性分析[J].软件学报, 2010, 21(7):1768-1782.LU F, ZHENG K F, NIU X X, et al. Security analysis of 3GPP authentication and key agreement protocol[J]. Journal of Software, 2010, 21(7):1768-1782.(in Chinese) [10] ZHANG M, FANG Y. Security analysis and enhancements of 3GPP authentication and key agreement protocol[J]. IEEE Transactions on Wireless Communications, 2005, 4(2):734-742. [11] 贾其兰, 白媛, 王倩, 等.UMTSAKA机制中序列号安全性分析[J].北京邮电大学学报, 2015, 38(S1):87-91.JIA Q L, BAI Y, WANG Q, et al. Security analysis of serial number in UMTSAKA mechanism[J].Journal of Beijing University of Posts and Telecommunications, 2015, 38(S1):87-91.(in Chinese) [12] 向东南, 毛文俊. LTE系统EPS-AKA过程安全性研究与改进[J].无线电通信技术, 2016, 42(5):60-63.XIANG D N, MAO W J. Research and improvement of EPS-AKA process security in LTE system[J].Radio Communication Technology, 2016, 42(5):60-63.(in Chinese) [13] BORGAONKAR R, HIRSCHI L, PARK S, et al. New privacy threat on 3G, 4G, and upcoming 5G AKA protocols[J]. Proceedings on Privacy Enhancing Technologies, 2019(3):108-127. [14] BASIN D, DREIER J, HIRSCHI L, et al. A formal analysis of 5G authentication[C]//2018 ACM SIGSAC Conference. Tornoto, Canada:ACM, 2018:1383-1396. [15] CREMERS C, DEHNEL-WILD M. Component-based formal analysis of 5G-AKA:Channel assumptions and session confusion[C]//Proceedings of the Network and Distributed System Security Symposium (NDSS).San Diego, USA:IEEE, 2019:23394. [16] 刘彩霞, 胡鑫鑫, 刘树新, 等. 基于Lowe分类法的5G网络EAP-AKA'协议安全性分析[J]. 电子与信息学报, 2019, 41(8):1800-1807.LIU C X, HU X X, LIU S X, et al. Security analysis of 5G network EAP-AKA' protocol based on lowe classification[J]. Journal of Electronics and Information Technology, 2019, 41(8):1800-1807.(in Chinese) [17] 3GPP. Security architecture and procedures for 5G system:3GPP TS 33.501[S]. Nice:ETSI, 2019. [18] LOWE G. A hierarchy of authentication specifications[C]//The 10th Computer Security Foundations Workshop, Rockport, USA, 1997:31-43. [19] DOLEV D, YAO A. On the security of public key protocols[J]. IEEE Transactions on Information Theory, 1981, 29(2):198-208.
2021, Vol. 61 
