# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 3 Formal Verification and Analysis of the 5G AKA Protocol  
To simplify the formal verification and analysis, we assume that:  
* The parties of the 5G AKA protocol shown in Figure 1 are simplified as the UE, the SN and the HN. The USIM and the ME are located in the UE, and the SEAF is located in the SN. The AUSF, the UDM, the ARPE and the SIDF are located in the HN. * There is a session key between the SN and the HN, and it is secure. * \(ngKS1\) and \(ABBA\) do not affect the security of the 5G AKA protocol, so they are ignored here. According to these assumptions, the 5G AKA protocol shown in Figure 1 can be summarized into three cases as follows: Case (I): the verification of \(AUTN\) succeeds and the authentication is successful. The steps of this case are as follows: 1. \(UE\to SN\): \(SUCI\); 2. \(SN\to HN\): \(\{SUCI||SNN\}_{K_{SN,HN}}\); 3. \(HN\to SN\): \(\{RAND||AUTN||HXRES^{*}\}_{K_{SN,HN}}\); 4. \(SN\to UE\): \(RAND||AUTN\); 5. \(UE\to SN\): \(RES^{*}\); 6. \(SN\to HN\): \(\{RES^{*}\}_{K_{SN,HN}}\); 7. \(HN\to SN\): \(\{Result||K_{SEAF}||SUPI\}_{K_{SN,HN}}\). where \(SUCI\), \(RAND||AUTN\) and \(RES^{*}\) are three messages exchanged between the UE and SN, \(\{SUCI||SNN\}_{K_{SN,HN}}\), \(\{RAND||AUTN||HXRES^{*}\}_{K_{SN,HN}}\), \(\{RES*\}_{K_{SN,HN}}\) and \(\{Result||K_{SEAF}||SUPI\}_{K_{SN,HN}}\) are four messages exchanged between the SN and the HN. Case (II): the verification of \(AUTN\) fails and it is a synchronization failure. The steps of this case are as follows: 1. \(UE\to SN\): \(SUCI\); 2. \(SN\to HN\): \(\{SUCI||SNN\}_{K_{SN,HN}}\); 3. \(HN\to SN\): \(\{RAND||AUTN||HXRES^{*}\}_{K_{SN,HN}}\); 4. \(SN\to UE\): \(RAND||AUTN\); 5. \(UE\to SN\): \(Syncf||AUTS\); 6. \(SN\to HN\): \(\{Syncf||RAND||AUTS\}_{K_{SN,HN}}\). RAND, AUTN, HXRES\({}^{*}\), Syncf, AUTS\(|\) with trace: \(<-\{SUCI||SNN\}_{K_{SN,HN^{\prime}}}\), \(+\{RAND||AUTN||HXRES^{*}\}_{K_{SN,HN^{\prime}}}\), \(-\{\textsf{Syncf}||RAND||AUTS\}_{K_{SN,HN}}>\). The principal associated with this strand is HN. **Definition 3**. : _A regular strand space \(\Sigma_{\textsf{III}}\) is a space for case III of the 5G AKA protocol if \(\Sigma_{\textsf{III}}\) is the union of three kinds of strands: (1) Initiator strands \(s\in\textsf{Init}_{\textsf{III}}[\)UE, SN, HN, SUCI, \(RAND\), \(AUTN\), \(MACf\)\(]\) with trace: \(<+SUCI\), \(-RAND||AUTN\), \(+MACf>\). The principal associated with this strand is UE. XMAC computed locally is not equal to \(MAC\subset AUTN\). (2) Responder strands \(r\in\text{Resp}_{\textsf{III}}[\)UE, SN, HN, SUCI, SNN, \(RAND\), H\({}_{1}\), H\({}_{2}\), \(MACf\)\(]\) with trace: \(<-SUCI\), \(+\{SUCI||SNN\}_{K_{SN,HN^{\prime}}}-\{RAND||H_{1}||H_{2}\}_{K_{SN,HN^{\prime}}}\), \(+RAND||H_{1}\), \(-MACf\), \(+\{MACf\}_{K_{SN,HN}}>\). The principal associated with this strand is SN. \(H_{1}\) and \(H_{2}\) are two messages that are not inspected by SN. (3) Server strands \(t\in\text{Serv}_{\textsf{III}}[\)UE, SN, HN, SUCI, SNN, \(RAND\), \(AUTN\), \(HXRES^{*}\), \(MACf\)\(]\) with trace: \(<-\{SUCI||SNN\}_{K_{SN,HN^{\prime}}}\), \(+\{RAND||AUTN||HXRES^{*}\}_{K_{SN,HN^{\prime}}}-\{MACf\}_{K_{SN,HN}}>\). The principal associated with this strand is HN._  
**Definition 4**. : _An infiltrated mixed strand space \(\sum\mathcal{P}\) is a space for the 5G AKA protocol if \(\sum=\sum_{\textsf{I}}\cup\sum_{\textsf{II}}\cup\sum_{\textsf{III}}\cup \mathcal{P}\), where penetrator strands \(p\in\mathcal{P}\)[28; 29; 30]._  
Definition 1 gives a regular strand space for case I of the 5G AKA protocol (i.e., \(\sum_{\textsf{I}}\)), including initiator strands, responder strands and server strands for case I of the 5G AKA protocol. Definition 2 gives a regular strand space for case II of the 5G AKA protocol (i.e., \(\sum_{\textsf{II}}\)), including initiator strands, responder strands and server strands for case II of the 5G AKA protocol.