A Formal Analysis Scheme for 5G Private Network Authentication Protocol

doi:10.3969/j.issn.1671-1122.2021.09.001

Abstract

Abstract:

This paper proposed a fine-grained formal modeling and verification scheme for the 5G EAP-TLS protocol. According to the TS 33.501 document, the scheme first constructed a protocol interaction model based on the Diffie-Hellman mode. Then the scheme expanded the Dolev-Yao model by introducing two participant compromised scenarios and mixed channel model. Finally, the verification tool SmartVerif was used to verify three types of security properties including confidentiality properties, authentication properties, and privacy properties. Experimental results show that the protocol exist safety flaws in terms of confidentiality properties and authentication properties. This paper analyzes the root causes of safety flaws and proposes a revised protocol. The revised protocol can meet all the security properties defined in the paper.

Key words: 5G private network, EAP-TLS authentication protocol, Dolev-Yao attacker model, formal method

CLC Number:

TP309

WANG Yuedong, XIONG Yan, HUANG Wenchao, WU Jianshuang. A Formal Analysis Scheme for 5G Private Network Authentication Protocol[J]. Netinfo Security, 2021, 21(9): 1-7.

Figures/Tables 11

References 13

[1]	BROEK F V D, VERDULT R, DE RUITER J. Defeating IMSI Catchers [C]//ACM. 22nd ACM SIGSAC Conference on Computer and Communications Security, October 12-16, 2015, Denver, CO, USA. New York: ACM, 2015: 340-351.
[2]	BLANCHET B. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules [C]//IEEE. 2001 IEEE Computer Security Foundations Symposium, June 11-13, 2001, Cape Breton, Nova Scotia, Canada. New Jersey: IEEE, 2001: 82-96.
[3]	CHEVAL V, KREMER S, RAKOTONIRINA I. DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice [C]//IEEE. 2018 IEEE Symposium on Security and Privacy(SP), May 21-23, 2018, San Francisco, California, USA. New Jersey: IEEE, 2018: 529-546.
[4]	BASIN D, DREIER J, HIRSCHI L, et al. A Formal Analysis of 5G [C]//ACM. 2018 ACM SIGSAC Conference on Computer and Communications Security, October 15-19, 2018, Toronto, ON, Canada. New York: ACM, 2018: 1383-1396.
[5]	MEIER S, SCHMIDT B, CREMERS C, et al. The TAMARIN Prover for the Symbolic Analysis of Security Protocols [C]//Springer. International Conference on Computer Aided Verification, July 13-19, 2013, Saint Petersburg, Russia. Heidelberg: Springer, 2013: 696-701.
[6]	CREMERS C, DEHNEL-WILD M. Component-based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion [C]//ISOC. Network and Distributed Systems Security(NDSS) Symposium, February 24-27, 2019, San Diego, California, USA. Rosten: ISOC, 2019: 1245-1260.
[7]	ZHANG Jiajing, WANG Qiang, YANG Lin, et al. Formal Verification of 5G-EAP-TLS Authentication Protocol [C]//IEEE. IEEE 4th International Conference on Data Science in Cyberspace(DSC), June 23-25, 2019, Hangzhou, China. New Jersey: IEEE, 2019: 503-509.
[8]	ZHANG Jiajing, WANG Qiang, YANG Lin, et al. Formal Analysis of 5G EAP-TLS Authentication Protocol Using ProVerif[EB/OL]. https://www.researchgate.net/publication/338985300_Formal_Analysis_of_5G_EAP-TLS_Authentication_Protocol_Using_Proverif, 2020-12-22.
[9]	CREMERS C. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols [C]//Springer. International Conference on Computer Aided Verification, July 7-14, 2008, Princeton, NJ, USA. Heidelberg: Springer, 2008: 414-418.
[10]	XIONG Yan, SU Cheng, HUANG Wenchao, et al. Smartverif: Push the Limit of Automation Capability of Verifying Security Protocols by Dynamic Strategies[EB/OL]. https://www.usenix.org/conference/usenixsecurity20/presentation/xiong, 2020-08-12.
[11]	DOLEV D, YAO Qizhi. On the Security of Public Key Protocols[J]. IEEE Transactions on Information Theory, 1983, 29(2): 198-208. doi: 10.1109/TIT.1983.1056650 URL
[12]	LOWE G. A Hierarchy of Authentication Specifications [C]//IEEE. 10th Computer Security Foundations Workshop, June 10-12, 1997, Rockport, MA, USA. New Jersey: IEEE, 1997: 31-43.
[13]	ARAPINIS M, MANCINI L, RITTER E, et al. New Privacy Issues in Mobile Telephony: Fix and Verification [C]//ACM. 2012 ACM Conference on Computer and Communications Security, October 16-18, 2012, Raleigh, NC, USA. New York: ACM, 2012: 205-216.

消息	形式化描述
Client/Server_Key_Exchange	g^c/g^s
R_PREKEY	g^cs
Certificate_UE/AUSF	sign(<SUPI, pkUE/pkAUSF>,ltkCA)
Client_Certificate_Verif	sign(hash(Previous),ltkUE)
Finished	senc(hash(Previous), K_SEAF)

等式	描述
(x^y)^z=x^yz	变量x的y次方的z次方等于x的yz次方
x¹=x	变量x的1次方等于x本身
xy=yx	等式满足交换律
(xy)z=x(yz)	等式满足结合律
xinv(x)=1	变量x与其逆相乘结果为1

信道	信道描述	建模假设
UE↔SEAF	无线空口链路,可能存在主动攻击者	公开信道
SEAF↔AUSF/ AUSF↔ARPF	有线链路,可提供保密、完整、重播保护	私密信道
UE↔CA/ ARPF↔CA	可信机构通过私密信道为参与方颁发证书	私密信道

设备	型号
CPU	Intel Broadwell E5-2620 v4 @2.10 GHz
内存容量	128 GB
操作系统	Ubuntu16.04 LTS
GPU	GeForce RTX 1080Ti（GPU显存11.0 GB）
底层验证工具	Tamarin-prover 1.5.1

密钥保密性	诚实参与方场景	UE受控场景	SEAF受控场景
S₁	√	-	√
S₂	√	-	√
S₃	√	-	×