Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model

The 5th generation mobile communication technology (5G) authentication and key management (AKA) protocol specified by the 3rd generation partnership project (3GPP) includes three cases because it introduces synchronization failure and message authentication code (MAC) failure procedures. Thus, 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 existing formal analysis and improvement of the 5G AKA protocol. To solve this problem, this paper formally analyzes the security of the latest version of the 5G AKA protocol based on the mixed strand space model for mixed protocols and finds many new attacks, including cross attacks for mixed cases. Then, a secure and efficient primary authentication and key agreement protocol for 5G networks is proposed, which is named the 5G-AKA'. In the 5G-AKA' protocol, the pre-shared key between the user equipment (UE) and the home network (HN) is replaced with a derivation key of the pre-shared key, the challenge-response mechanism between the serving network (SN) and the HN is added, the subscription permanent identifier (SUPI) of the UE is added to the second message between the SN and the HN, and the MAC failure is replaced with a timeout mechanism on the HN. Finally, the 5G-AKA' protocol is proved secure in the mixed strand space model and can overcome these attacks of the latest version of the 5G AKA protocol. Additionally, the comparative analysis shows that the 5G-AKA' protocol is better than the recently improved 5G AKA protocols in security, and the 5G-AKA' protocol is efficient and is backward compatible with the 5G AKA protocol.