# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 2 Overview of the 5G AKA Protocol  
According to [2; 3; 4], the steps of the latest version of the 5G AKA protocol in the 3 GPP standard version v17.4.0 of TS 33.501 are illustrated in Figure 1.  
In Figure 1, the detailed steps of the latest version of the 5G AKA protocol are as follows:  
Figure 1: The steps of the latest version of the 5G AKA protocol. In the following notations, various fields in the figures have been described, including these fields marked with *. In detail, \(XRES\) is an expected response, while \(XRES^{*}\) is an expected response from \(XRES\), then \(HXRES^{*}\) is a hashing expected response from \(XRES^{*}\). \(RES\) is response, while \(RES^{*}\) is a response from \(RES\). When the security anchor function (SEAF) initiates authentication with the user equipment (UE), the UE sends \(SUCI\) to the SEAF, where the UE includes mobile equipment (ME) and a universal subscriber identity module (USIM). \[SUCI=x\cdot G||\{SUPI\}_{EK}||MAC_{UE} \tag{1}\]  
\[EK||ICB||MK=KDF(x\cdot y\cdot G) \tag{2}\]  
\[MAC_{UE}=HMAC(MK,\{SUPI\}_{EK}) \tag{3}\]  
where \(SUCI\) denotes a SUCI of the UE, \(SUPI\) denotes the subscription permanent identifier (SUPI) of the UE, \(x\cdot G\) and \(x\) are an ephemeral public/private key pair of the UE for the Diffie-Hellman exchange, \(y\cdot G\) and \(y\) are an ephemeral public/private key pair of the home network (HN) for the Diffie-Hellman exchange, \(EK\) is an encryption key, \(ICB\) is an initial counter block (ICB), \(MK\) is a MAC key, \(MAC_{UE}\) is a MAC of the UE, \(KDF()\) is a key derivation function and \(HMAC()\) is a hash function for computing MAC, \(||\) denotes a cascade of fields. 2. Upon receiving \(SUCI\), the SEAF sends \(SUCI\) and \(SNN\) to the authentication server function (AUSF). \(SNN\) denotes the serving network name (SNN) of the SN. 3. If the SEAF is entitled to use \(SNN\), then the AUSF stores the receiving \(SNN\) and sends \(SUCI\) and \(SNN\) to the unified data management (UDM). 4. The UDM invokes the subscriber identity de-concealing function (SIDF) whether \(SUCI\) is received. Then, the SIDF de-conceals \(SUCI\) to gain \(SUPI\) before the UDM can process the request. Based on \(SUPI\), the UDM/ARPF (authentication credential repository and processing function) chooses the authentication method. 5. When 5G AKA is selected, the UDM/ARPF generates \(RAND\), calculates \(AUTN\) and \(XRES^{*}\), and derives \(K_{AUSF}\), and then creates a 5G home environment authentication vector from \(RAND\), \(AUTN\), \(XRES^{*}\) and \(K_{AUSF}\). \(RAND\) is an unpredictable challenge of the HN. \[AUTN=SQN\oplus AK||AMF||MAC\] (4) \[MAC=f_{1}(K,SQN||RAND||AMF)\] (5) \[XRES=f_{2}(K,RAND)\] (6) \[CK=f_{3}(K,RAND)\] (7) \[IK=f_{4}(K,RAND)\] (8) Figure 1:0 (9) Figure 1:1 (10) Figure 1:2 (11)  
where \(AUTN\) is an authentication token of the HN, \(SQN\) is a fresh sequence number generated by the HN, \(AK\) is an anonymity key, \(AMF\) is the authentication management field (AMF) and the separation bit of the AMF is set 1, \(MAC\) is a MAC of the HN, \(K\) is a long-term key between the UE and the HN, \(f_{1}()\) and \(f_{2}()\) are two message authentication functions, \(f_{3}()\), \(f_{4}()\) and \(f_{5}()\) is three key generating functions, \(CK\) is a cipher key, \(IK\) is an integrity key, \(K_{AUSF}\) is a key derived from \(CK\) and \(IK\), \(XRES\) is an expected response and \(XRES^{*}\) is an expected response derived from \(CK\) and \(IK\). 6. The UDM sends the 5G home environment authentication vector to the AUSF together with \(SUPI\). When an authentication and key management for applications (AKMA) subscription is used, the UDM also sends \(AKMA\) to the AUSF. \(AKMA\) denotes the AKMA indication and routing indicator. 7. The AUSF stores the \(XRES^{*}\) temporarily together with the received \(SUPI\). 8.