# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 3 Formal Verification and Analysis of the 5G AKA Protocol
### The Server's Guarantee of the 5G AKA Protocol  
**Theorem 4. **_Suppose: (1) \(\sum\) is a space for the 5G AKA protocol, and \(\mathcal{C}\) is a bundle containing a server strand \(t\in Serv_{l}[UE,\) SN, \(HN,\) SUC1, \(SNN,\) RAND, \(AUTN,\)\(HXRES^{*},\)\(RES^{*},\)\(Result,\)\(K_{\mathit{SEAF}},\)\(SUPI]\); (2) \(K\
otin\mathcal{K}_{P}\) and \(K_{\mathit{SN}^{*}HN}\
otin\mathcal{K}_{P}\), where \(\mathit{SN}^{*}\) denotes any authorized SN; (3) \(RAND\) is uniquely originating in \(\sum\). Then, \(\mathcal{C}\) contains an initiator strand \(s\in\text{Init}_{l}[UE,\) SN, \(HN,\)\(SUC1^{\prime},\)\(RAND,\)\(AUTN,\)\(RES^{*}]\) and a responder strand \(r\in\text{Resp}_{l}[UE^{\prime},\)\(SN,\)\(HN,\)\(SUC1^{\prime\prime},\)\(SNN,\)\(RAND,\)\(AUTN,\)\(HXRES^{*},\)\(RES^{*},\)\(Result,\)\(K^{\prime}\)\({}_{\mathit{SEAF}},\)\(SUPI^{\prime\prime}]\), where \(x^{\prime}\subset SUC1^{\prime}\), \(SUPI^{\prime\prime}\subset SUC1^{\prime\prime}\) and \(K^{\prime\prime}\)\({}_{\mathit{SEAF}}\) is generated for \(\mathit{SUPI^{\prime\prime}}\)._  
**Proof of Theorem 4. ** By assumption (2), \(K\
otin\mathcal{K}_{P}\). Since \(CK=f_{3}(K,RAND)\) and \(IK=f_{4}(K,RAND)\), \(CK\
otin\mathcal{K}_{P}\) and \(IK\
otin\mathcal{K}_{P}\), so \(CK||IK\
otin\mathcal{K}_{P}\). Hence, \(RES^{*}=KDF(CK||IK,SNN||RAND||RES)\subset term(<t,3>)\) must originate on an initiator strand \(s\in\text{Init}_{l}[UE,\)\(SN,\)\(HN,\)\(SUC1^{\prime},\)\(RAND,\)\(AUTN^{\prime},\)\(RES^{*}]\), where \(x^{\prime}\subset SUC1^{\prime}\) and \(\mathit{SQN}^{\prime}\subset AUTN^{\prime}\). Since \(K\
otin\mathcal{K}_{P}\), \(MAC^{\prime}=f_{1}(K,\mathit{SQN}^{\prime}||RAND||AMF)\subset AUTN^{\prime} \subset term(<s,2>)\) must originate on a server strand \(t^{\prime}\). Since \(RAND\) is uniquely originating in \(\sum\)\(t^{\prime}=t\), so \(\mathit{SQN}^{\prime}=\mathit{SQN}\) and \(AUTN^{\prime}=AUTN\). Hence, \(s\in\text{Init}_{l}[UE,\)\(SN,\)\(HN,\)\(SUC1^{\prime},\)\(RAND,\)\(AUTN,\)\(RES^{*}]\). By assumption (2), \(K_{\mathit{SN}HN}\
otin\mathcal{K}_{P}\), so \(\{RES^{*}\}_{K_{\mathit{SN}HN}}=\mathit{term}(<t,3>)\) must originate on a responder strand \(r\in\text{Resp}_{l}[UE^{\prime},\)\(SN,\)\(HN,\)\(SUC1^{\prime\prime},\)\(SNN,\)\(RAND,\)\(H^{\prime\prime}\)\({}_{\mathit{1}},HXRES^{*},\)\(RES^{*},\)\(Result,\)\(K^{\prime\prime}\)\({}_{\mathit{SEAF}},\)\(SUPI^{\prime\prime}]\), where \(SUPI^{\prime\prime}\subset SUC1^{\prime\prime}\) and \(K^{\prime\prime}\)\({}_{\mathit{SEAF}}\) is generated for \(SUPI^{\prime\prime}\). Since \(K_{\mathit{SN}HN}\
otin\mathcal{K}_{P}\), \(\{RAND||H^{\prime\prime}||HXRES^{*}\}_{K_{\mathit{SN}HN}}=\mathit{term}(<r,3>)\) must originate on a server strand \(t^{\prime\prime}\). Since \(RAND\) is uniquely originating in \(\sum\)\(t^{\prime}=t\), so \(H^{\prime\prime}\)\({}_{\mathit{1}}=AUTN\). Hence, \(r\in\text{Resp}_{l}[UE^{\prime},\)\(SN,\)\(HN,\)\(SUC1^{\prime\prime},\)\(SNN,\)\(RAND,\)\(AUTN,\)\(HXRES^{*},\)\(RES^{*},\)\(Result,\)\(K^{\prime\prime}\)\({}_{\mathit{SEAF}},\)\(SUPI^{\prime\prime}]\). \(\square\)  
According to Theorem 4, the corresponding attack scenario can be obtained as shown in Figure 12, where the messages between the HN and the authorized SN are protected by their session key. Figure 11: The tenth attack scenario of the 5G AKA protocol. In Figure 12, the green dashed box represents the server strand of Theorem 4, while the blue dashed boxes represent the initiator strand and the responder strand of Theorem 4. The fields marked in red on the initiator strand and the responder strand are some fields that cannot be agreed with the HN, which are caused by MitM attacks. According to Figure 12, \(HN\) successfully authenticates \(UE\) and \(SN\), but some specific attacks can be found as follows:  
1. \(HN\) cannot find that \(SUCI\) is replayed, which is not equal to \(SUCI^{\prime}\) and \(SUCI^{\prime\prime}\). This is because \(SUCI\) does not contain the challenge of the HN (i.e., \(RAND\)).