# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 3 Formal Verification and Analysis of the 5G AKA Protocol
### The Respender's Guarantee of the 5G AKA Protocol
Since \(CK^{\prime}=f_{3}(K^{\prime},RAND)\) and \(IK^{\prime}=f_{4}(K^{\prime},RAND)\), \(CK^{\prime}\
otin\mathcal{K}_{P}\) and \(IK^{\prime}\
otin\mathcal{K}_{P}\), so \(CK^{\prime}||IK^{\prime}\
otin\mathcal{K}_{P}\). Hence, \((RES^{*})^{\prime}=term(<r,5>)\) must originate on an initiator strand \(s\in\text{Init}_{\uparrow}[UE^{\prime},SN,HN,SUCI^{\prime\prime},RAND,AUTN^{ \prime\prime},(RES^{*})^{\prime}]\), where \(SUPI^{\prime}\subset SUCI^{\prime\prime}\) and \(SQN^{\prime\prime}\subset AUTN^{\prime\prime}\). Since \(K^{\prime}\
otin\mathcal{K}_{P}\), \(MAC^{\prime\prime}=f_{1}(K^{\prime},SQN^{\prime\prime}||RAND||AMF)\subset AUTN^{ \prime\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\prime}=SQN\) and \(AUTN^{\prime\prime}=AUTN^{\prime}\). Hence, \(s\in\text{Init}_{\uparrow}[UE^{\prime},SN,HN,SUCI^{\prime},RAND,AUTN^{\prime},(RES^{*})^{\prime}]\). \(\square\)  
According to Theorem 7, the corresponding attack scenarios can be obtained as shown in Figures 15 and 16, where the messages between the HN and the authorized SN are protected by their session key. In Figures 15 and 16, the green dashed box represents the responder strand of Theorem 7, while the blue dashed boxes represent the initiator strand and the server strand of Theorem 7. The fields marked in red on the initiator strand and the server strand are some fields that cannot be agreed with the SN, which are caused by MitM attacks. According to Figures 15 and 16, some specific attacks can be found as follows:  
1. \(SN\) successfully authenticates \(HN\), but does not authenticate \(UE\). This is because \(SN\) cannot inspect \(AUTN^{\prime}\), \((HXRES^{*})^{\prime}\) and \((RES^{*})^{\prime}\), and \(SUPI\) is not sent with \(RAND\), which means that \(AUTN^{\prime}\), \((HXRES^{*})^{\prime}\) and \((RES^{*})^{\prime}\) can be related to \(SUPI^{\prime}\) rather than \(SUPI\). Accordingly, \(SUPI^{\prime}\) is included in \(SUCI^{\prime}\) and \(SUCI^{\prime}\), and is related to \(K^{\prime}_{SEAF}\). That is to say, the authentication fails, resulting in a new authentication and key agreement process. 2. In Figure 16, there are interactions between different cases of the 5G AKA protocol, i.e., cross attacks. They are caused by the penetrators taking advantage of \(MACf\). The penetrator replays an encrypted \(MACf\) between the SN and the HN to make  
Figure 16: The fifteenth attack scenario of the 5G AKA protocol. Figure 15: The fourteenth attack scenario of the 5G AKA protocol. authentication failure, i.e., MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process. 3. The initiator strand and the server strand of Theorem 7 may exist in the past run of the protocol because they do not contain the challenge of the SN, i.e., the messages received by the SN can be replayed messages. As a result, the penetrator can impersonate the UE and the HN to complete the entire 5G AKA protocol with the SN, forming DoS attacks on the SN. This results in the energy consumption ion of the SN. Theorem 7: _Suppose: (1) \(\sum\) is a space for the 5G AKA protocol, and \(\mathcal{C}\) is a bundle containing a responder strand \(r\in\text{Resp}_{\Pi}[\text{UE},\,SN,\,HN,\,\text{SUCI},\,SNN,\,RAND,\,H_{1},\,H_{2 },\,S\!\text{y}\!\text{c}f,\,H_{4}]\); (2) \(K^{*}\
otin\mathcal{K}_{p}\) and \(K_{\text{SN}^{*},HN}\
otin\mathcal{K}_{p}\), where \(SN^{*}\) denotes any authorized SN and \(K^{*}\) denotes a pre-shared key between HN and any authorized UE; (3) \(RAND\) is uniquely originating in \(\sum\).