# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 6 Conclusions  
In this paper, we summarize the 5G AKA protocol into three cases according to the overview of the latest version of the 5G AKA protocol and then use the mixed strand space model for mixed protocols to formally analyze the security of the 5G AKA protocol. As a result, twenty-one attack scenarios of the 5G AKA protocol are obtained, where thirteen attack scenarios are related to the MAC failure, including MAC failure attacks. Based on these attack scenarios, we find that the mutual authentication between the UE and the SN cannot be established, and only the weaker agreement can be established among the UE, the SN and the HN, resulting in MitM attacks and cross attacks. Further, by replaying some message to the UE and the SN, replay attacks and masquerading attacks can be performed, the location privacy of the UE can be compromised and DoS attacks on the SN can be formed. In addition, the 5G AKA protocol cannot provide perfect forward secrecy.  
To overcome these attacks, we propose a 5G-AKA' protocol, in which the pre-shared key between the UE and the HN is replaced with a derivation key of the pre-shared key, the challenge-response mechanism between the SN and the HN is added, the SUPI of the UE is added to the second message between the SN and the HN, and the MAC failure procedure is replaced with a timeout mechanism on the HN. According to the 5G-AKA' protocol, we summarize the 5G-AKA' protocol into two cases and then use the mixed strand space model for mixed protocols to formally analyze the security of the 5G-AKA' protocol. As a result, no attack scenario is obtained.  
By discussion and analysis, the 5G-AKA' protocol can establish mutual authentication and injection agreement among the UE, the SN and the HN, and can overcome the above security problems of the latest version of the 5G AKA protocol. Therefore, the 5G-AKA' protocol is secure. The comparative analysis of security properties between the 5G-AKA' protocol and some recently improved 5G AKA protocols shows that the 5G-AKA' protocol is better than these recently improved 5G AKA protocols in security. The comparative analysis between the 5G-AKA' protocol and some recently improved 5G AKA protocols in the number of messages, the number of fields, the amount of calculation and backward compatibility shows that the 5G-AKA' protocol is efficient, and is backward compatible with the 5G AKA protocol.  
Recently, some authors also point out that the protection mechanism of SQN can be defeated due to its use of XOR in the 5G AKA protocol. This paper does not consider this security problem, and we will further study this security problem in the future.  
**Funding:** This research was funded by the National Natural Science Foundation of China (No.61741216, 61402367), Shaanxi Science and Technology Co-ordination & Innovation Project (No.2016 KTTSGY01-03), National Key Research and Development Program (No. 2018 YFC08242-04) and New Star Team Project of Xi'an University of Posts and Telecommunications.  
**Institutional Review Board Statement:** Not applicable.  
**Informed Consent Statement:** Not applicable.  
**Data Availability Statement:** Not applicable.  
**Conflicts of Interest:** The authors declare no conflict of interest.