# 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
That is to say, the replay attacks on the HN can be formed, resulting in the energy consumption ion of the HN. 2. \(K^{\prime\prime}\)\({}_{SEAF}\) and \(SUPI^{\prime\prime}\) cannot be agreed with the HN because the HN does not send \(K^{\prime\prime}\)\({}_{SEAF}\) and \(SUPI^{\prime\prime}\) together with \(RAND\), which makes that \(K^{\prime\prime}\)\({}_{SEAF}\) and \(SUPI^{\prime\prime}\) can be a replayed key and a replayed SUPI, respectively. That is to say, the key agreement fails, resulting in a new authentication and key agreement process. **Theorem 5**. : _Suppose: (1) \(\sum\) is a space for the 5G AKA protocol, and \(\mathcal{C}\) is a bundle containing a server strand \(t\in\text{Ser}_{\Pi}[UE,\) SN, \(HN,\) SUCI, \(SNN,\) RAND, \(AUTN,\)\(HXRES^{*},\)\(S\)\(\forall\)\(\mathit{AUTS}]\); (2) \(K\
otin\mathcal{K}_{P}\) and \(K_{SNs,HN}\
otin\mathcal{K}_{P}\), where \(SN^{*}\) denotes any authorized SN; (3) \(RAND\) is uniquely originating in \(\sum\). Then, \(\mathcal{C}\) contains an initiator strand \(s\in\text{Init}_{\Pi}[UE,\) SN\({}^{\prime},\)\(HN,\)\(SUCI^{\prime},\)\(RAND,\)\(AUTN,\)\(S\)\(\forall\)\(\mathit{AUTS}]\) and a responder strand \(r\in\text{Resp}_{\Pi}[UE^{\prime},\) SN, \(HN,\)\(SUCI^{\prime},\)\(SNN,\)\(RAND,\)\(AUTN,\)\(HXRES^{*},\)\(S\)\(\forall\)\(\mathit{SUCI}^{\prime},\)\(AUTS]\), where \(x^{\prime}\subset SUCI^{\prime}\) and \(SUPI^{\prime\prime}\subset SUCI^{\prime}\)._  
Proof of Theorem 5.: By assumption (2), \(K\
otin\mathcal{K}_{P}\), so \(MAC-S=f_{1}^{*}(K,SQN_{UE}\big{|}\big{|}RAND\)\(||AMF_{0})\)\(\subset AUTS\subset term(<t,3>)\) must originate on an initiator strand \(s\in\text{Init}_{\Pi}[UE,\)\(SN^{\prime},\)\(HN,\)\(SUCI^{\prime},\)\(RAND,\)\(AUTN^{\prime},\)\(S\)\(\forall\)\(\mathit{AUTS}]\), where \(x^{\prime}\subset SUCI^{\prime}\) and \(SQN^{\prime}\subset AUTN^{\prime}\). Since \(K\
otin\mathcal{K}_{P}\), \(MAC^{\prime}=f_{1}(K,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 \(SQN^{\prime}=SQN\) and \(AUTN^{\prime}=AUTN\). Hence, \(s\in\text{Init}_{\Pi}[UE,\)\(SN^{\prime},\)\(HN,\)\(SUCI^{\prime},\)\(RAND,\)\(AUTN,\)\(S\)\(\forall\)\(\mathit{AUTS}]\). By assumption (2), \(K_{SN,HN}\
otin\mathcal{K}_{P}\), so \(\{S\)\(\forall\  
\(RAND\) is uniquely originating in \(\sum t^{\prime\prime}=t\), so \(H^{\prime\prime}{}_{1}=AUTN\) and \(H^{\prime\prime}{}_{2}=HXRE^{*}\). Hence, \(r\in\text{Resp}_{\Pi}[UE^{\prime\prime},\,SN,\,HN,\,SUCI^{\prime\prime},\,SNN, \,RAND,\,AUTN,\,HXRE^{*},\,Syncf,\,AUTS]\). \(\square\)  
According to Theorem 5, the corresponding attack scenario can be obtained as shown in Figure 13, where the messages between the HN and the authorized SN are protected by their session key. In Figure 13, the green dashed box represents the server strand of Theorem 5, while the blue dashed boxes represent the initiator strand and the responder strand of Theorem 5. 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 13, \(HN\) successfully authenticates \(UE\) and \(SN\). However, \(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\)). That is to say, the replay attacks on the HN can be formed, resulting in the energy consumption ion of the HN. **Theorem 6**. : _Suppose: (1) \(\sum\) is a space for the 5G AKA protocol, and \(\mathcal{C}\) is a bundle containing a server strand \(t\in\text{Serv}_{\Pi}[UE,\,SN,\,HN,\,SUCI,\,SNN,\,RAND,\,AUTN,\,HXRE^{*},\, MACf]\); (2) \(K_{SN^{*},HN}\
otin\mathcal{C}_{P}\), where \(SN^{*}\) denotes any authorized SN.