# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 1 Introduction
In [23], [PERSON] et al. discovered an attack exploiting the subscription concealed identifier (SUCI) to track a subscriber in the 5G network, which is directly caused by the insecure air channel. To cover this issue, they proposed a secure authentication scheme by utilizing the existing public key infrastructure (PKI) mechanism. Further, they found a location sniffing attack, which can be implemented by an attacker through inexpensive devices [24]. Similarly, they proposed a fix scheme based on the existing PKI mechanism. In [25], [PERSON] et al. modeled the 5G AKA protocol with symbolic modeling using ProVerif based on three and four entities models, and then proposed their security consideration. Further, [PERSON] et al. [26] proposed an enhanced version of the authentication and key agreement protocol for the 5G system that surmounts the limitations existing in the 5G AKA protocol. [PERSON] et al. [27] introduced a protocol that preserves the privacy of the user identity and overcomes the identified problems of the 5G AKA protocol. Similarly, 3 GPP has also been enhancing the security of the 5G AKA protocol [2; 3; 4]. Because the 5G AKA protocol [2; 3; 4] introduces synchronization failure and message authentication code (MAC) failure procedures, it has three cases, so there may be interactions between these cases, forming vulnerabilities that do not exist in any single case. However, this is not fully considered in the above security analysis and improvement of the 5G AKA protocol. Therefore, we formally analyze the security of the latest version of the 5G AKA protocol considering three cases at the same time. Then, we propose a secure and efficient primary authentication and key agreement protocol for 5G networks, namedthe 5G-AKA'. Finally, we prove that the 5G-AKA' protocol is secure, and it is efficient and backward compatible. The main contributions of this paper are as follows:  
* We formally analyze the security of the latest version of the 5G AKA protocol in the mixed strand space model for mixed protocols [28] and give twenty-one attack scenarios of the 5G AKA protocol. Based on these attack scenarios, we find many new attacks of the 5G AKA protocol, including cross attacks for mixed cases. * We propose the 5G-AKA' protocol, and then formally analyze its security in the mixed strand space model for mixed protocols [28]. As a result, no attack scenario is obtained. By discussion and analysis, the 5G-AKA' protocol can overcome these attacks of the 5G AKA protocol, thus it is secure. * Based on comparative analysis, the 5G-AKA' protocol is better than the 5G AKA protocol and the recently improved 5G AKA protocols in security, and is efficient and backward compatible. The rest of this paper is organized as follows. Section 2 provides an overview of the latest version of the 5G AKA protocol. In Section 3, we formally analyze the security of the latest version of the 5G AKA protocol in the mixed strand space model. Section 4 describes our proposed 5G-AKA' protocol and gives the security analysis of the 5G-AKA' protocol in the mixed strand space model. In Section 5, we present some discussions and we conclude the paper in Section 6.