# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 2 Overview of the 5G AKA Protocol
The AUSF generates a 5G authentication vector from the 5G home environment authentication vector received from the UDM/ARPF by computing \(HXRES^{*}\) from \(XRES^{*}\), computing \(K_{SEAF}\) from \(K_{AUSF}\), replacing \(XRES^{*}\) with \(HXRES^{*}\), and replacing \(K_{AUSF}\) with \(K_{SEAF}\) in the 5G home environment authentication vector. Figure 1:3  
Figure 1:4  
where \(HXRES^{*}\) is a hashing \(XRES^{*}\), \(SHA256()\) is a hash function. 9. The ASUF creates a 5G serving environment authentication vector by removing \(K_{SEAF}\) from the 5G authentication vector, and then sends the 5G serving environment authentication vector (i.e., \(RAND\), \(AUTN\) and \(HXRES^{*}\)) to the SEAF. 10. The SEAF stores \(HXRES^{*}\), and then sends \(RAND\), \(AUTN\), \(ngKSI\) and \(ABBA\) to the UE. \(ngKSI\) is used by the UE and the access and mobility management function to identify the \(K_{AMF}\) and the partial native security context that is created if the authentication is successful. \(ABBA\) denotes the anti-bidding down between architectures (ABBA) parameter. 11. In the UE, the ME forwards \(RAND\) and \(AUTN\) to the USIM. Upon receipt of \(RAND\) and \(AUTN\), the USIM first computes the anonymity key \(AK\) and retrieves the sequence number \(SQN\). Next, the USIM computes \(XMAC\) and compares this with \(MAC\) which is included in \(AUTN\). Then, the USIM verifies that the received \(SQN\) is in the correct range. If \(XMAC\) is the same as \(MAC\) and \(SQN\) is in the correct range (i.e., \(SQN_{UE}<SQN\), where \(SQN_{UE}\) denotes the highest sequence number the USIM has accepted), then the USIM computes a response \(RES\), \(CK\) and \(IK\), and then returns \(RES\), \(CK\) and \(IK\) to the ME. The ME then computes \(RES^{*}\), \(K_{AUSF}\) and \(K_{SEAF}\). Figure 1:5 (14)  
Figure 1:6  
Figure 1:7  
where \(RES\) is a response and \(RES^{*}\) is a response derived from \(CK\) and \(IK\). 12. The UE sends \(RES^{*}\) to the SEAF. 13. The SEAF computes \(HRES^{*}\) and compares this with \(HXRES^{*}\). If they coincide, then the SEAF considers the authentication as successful from the serving network's point of view. If not, then the SEAF considers the authentication as unsuccessful. Figure 1:8 (17) where \(HRES^{*}\) is a hashing \(RES^{*}\). 14. The SEAF sends the received \(RES^{*}\) to the AUSF. 15. The AUSF compares the received \(RES^{*}\) with the stored \(XRES^{*}\). If \(RES^{*}\) and \(XRES^{*}\) are equal, then the AUSF considers the authentication as successful from the home network point of view. Then, the AUSF informs the UDM about the authentication result. 16. The AUSF indicates to the SEAF whether the authentication was successful or not from the home network point of view (i.e., \(Result\)). If the authentication was successful, then the ASUF also sends \(K_{SEAF}\) and \(SUPI\) to the SEAF. In step 11, if \(XMAC\) and \(MAC\) are different, then the USIM indicates to the ME a MAC failure of \(AUTN\). Then, the UE sends the \"MAC failure\" indication to the SEAF. Further, the SEAF sends the \"MAC failure\" indication to the AUSF. Finally, the ASUF sends the \"MAC failure\" indication to the UDM/ARPF. In step 11, if \(SQN\) is not in the correct range (i.e., \(SQN_{UE}\geq SQN\)), then the USIM computes \(AUTS\), and then sends \(AUTS\) with a \"Synchronization failure\" indication to the ME. Then, the UE sends \(AUTS\) with the \"Synchronization failure\" indication to the SEAF. Further, the SEAF sends \(RAND\) and \(AUTS\) with the \"Synchronization failure\" indication to the AUSF. Finally, the ASUF sends \(RAND\) and \(AUTS\) with the \"Synchronization failure\" indication to the UDM/ARPF. Figure 1:9  
\[SUCI=x\cdot G||\{SUPI\}_{EK}||MAC_{UE} \tag{1}\]0  
\[SUCI=x\cdot G||\{SUPI\}_{EK}||MAC_{UE} \tag{1}\]1  
where \(AK^{*}\) is an anonymity key, \(MAC-S\) is a MAC of the UE, \(AMF_{0}\) is a dummy value of all zeros, \(f_{1}^{*}()\) is a message authentication function and \(f_{5}^{*}()\) is a key generating function.