# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 1 Introduction  
With the continuous popularization of the 5 th generation mobile communication technology (5G), in the near future, the 5G network, as an important communication infrastructure, will penetrate into diversified vertical industries and fields such as transportation, medical treatment and industry, and support various information interactions between people, people and things, and things and things and things [1]. In the 5G network, three different primary authentication and key agreement protocols are defined in the related 3 rd generation partnership project (3 GPP) specifications [2; 3; 4], including the 5G authentication and key agreement (AKA) protocol, the improved extensible authentication protocol method for 3 rd generation authentication and key agreement (EAP-AKA) protocol and the 5G extensible authentication protocol method for transport layer security (EAP-TLS) protocol. The first two protocols are based on the shared key cryptography, while the last one is based on the public key cryptography. These protocols all aim to provide mutual authentication of subscribers and networks. Currently, they are in the process of standardization. The 5G AKA protocol [2; 3; 4] is developed directly from the evolution packet system (EPS)-AKA protocol of the long-term evolution (LTE)/4 th generation mobile communication technology (4G) network [3], so it inherits certain security vulnerabilities from the EPS-AKA protocol such as impersonation attacks, man-in-the-middle attacks (MitM) and denial of service (DoS) attacks [5; 6; 7; 8; 9; 10; 11]. [PERSON] et al. [12] analyzed the 5G AKA protocol of technical specification (TS) 33.501 v0.7.0. They discovered a protocol vulnerability that would enable the attacker to impersonate another user to a serving network (SN). Based on the Tamarin model checker [13], [PERSON] et al. [14] investigated the security properties of the 5G AKA protocol of TS 33.501 v15.1.0, and several major issues were revealed, which are related to user localization, leakage of activity, the impact of active attackers and the presence of malicious SN while roaming. In [15], [PERSON] et al. pointed out that the 5G AKA protocol suffers from link-ability attacks, and then proposed a new authentication scheme by making use of the Diffie-Hellman key exchange algorithm for generating the session key. This scheme was successful in preventing link-ability attacks along with a MitM attack. For the more recent 5G AKA protocol, [PERSON] et al. [16] found a new attack. They claimed that the protection mechanism of the sequence number (SQN) can be defeated under specific replay attacks due to its use of exclusive-or (XOR) and a lack of randomness. In [17], [PERSON] et al. modeled all the key components of the 5G AKA protocol (i.e., the user equipment, the serving network and the home network) according to the definition in the 3 GPP specification document. They discovered an attack that exploits a potential race condition and additionally showed that solving the race condition for the honest case does not necessarily prevent the attack. In [18], [PERSON] et al. investigated the privacy properties of the 5G AKA protocol using the Bana-Comon logic [19; 20]. They discovered a novel de-synchronization attack and proved that their proposed protocol guarantees the privacy properties. In [21], [PERSON] et al. proposed a novel version of the 5G AKA protocol to prevent active attacks and gain resistance against malignant serving networks. Unfortunately, there is a possibility of having SN impersonation, so this scheme does not eliminate the vulnerability towards the MitM attack. Further, [PERSON] et al. [22] also attempted to launch a revised version of the 5G AKA protocol. However, their proposed protocol suffers from privacy preservation as the device identities are clearly transmitted in the air which leads to numerous security attacks. As time goes on, more and more attacks of the 5G AKA protocol were found due to the insecure channel between different network domains in the legacy mobile network.