Paper Info
Title
A Systematic Analysis Method for 5G Non-Access Stratum Signalling Security
Abstract
This paper proposes a systematic analysis method for 5G Non-Access Stratum Signalling security based on formal analysis, which has identified 10 new 5G protocol vulnerabilities, and an improved PKI security mechanism targeted at eliminating these vulnerabilities. Firstly, the 5G system, state transition properties and security properties were abstracted from 3GPP specifications. To mimic an attacker's behavior, a Dolev-Yao adversary model was constructed in the 5G model by empowering it with NAS signalling security testing knowledge and reasonable security capabilities in the wireless channel. Then we used the TAMARIN prover to verify all the abstracted properties one by one and discovered some protocol vulnerabilities based on the counterexamples found. We further verified these vulnerabilities on the testbed and identified 10 new 5G protocol vulnerabilities. Moreover, we analyzed the root cause of these vulnerabilities and concluded that all of them were caused by the unconditional trust between UE and gNodeB. Therefore, we propose an improved PKI mechanism based on the existing asymmetric encryption of 5G. Besides the existing public-private key pair of the home network, we introduce a new pair of asymmetric keys in the gNodeB to encrypt and sign the signalling message sent to UE. The gNodeB can be connected only when the verification succeeds and then the RRC connection can be initiated. This mechanism can effectively avoid all the vulnerabilities found in this paper.
Year
DOI
Venue
2019
10.1109/ACCESS.2019.2937997
IEEE ACCESS
Keywords
DocType
Volume
5G,protocol security,privacy,NAS,formal method,public key infrastructure
Journal
7
ISSN
Citations 
PageRank 
2169-3536
0
0.34
References 
Authors
0
6
Name
Order
Citations
PageRank
Xinxin Hu1566.54
Caixia Liu261.49
Shuxin Liu3294.17
Wei You4114.20
Yingle Li500.34
Yu Zhao66120.45