# 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
If \(t\) is a server strand of Definition 2, then \(t\in\text{Serv}_{\Pi}[\text{UE}^{\prime},\,SN,\,HN,\,\text{SUCI}^{\prime},\, SNN,\,RAND,\,AUTN^{\prime},\,(HXRES^{*})^{\prime},\,S\!\text{y}\!\text{c}f,\, AUITS^{\prime}]\), where \(SUP^{\prime}\subset\text{SUCI}^{\prime},\,K^{\prime}\subset AUTN^{\prime},\,K^{ \prime}\subset(HXRES^{*})^{\prime}\), \(K^{\prime}\subset AUTN^{\prime}\) and \(SQN_{\text{UE}^{\prime}}\subset AUTS^{\prime}\). By assumption (2), \(K^{\prime}\
otin\mathcal{K}_{p}\), so \((MAC-S)^{\prime}=f_{1}^{*}(K^{\prime},SQN_{\text{UE}^{\prime}}||RAND||AMF_{0}) \subset AUTS\subset term(<t,3>)\) must originate on an initiator strand \(s\in\text{Init}_{\Pi}[\text{UE}^{\prime},\,SN^{\prime\prime},\,HN,\,\text{SUCI}^{\prime},\,RAND,\, AUTN^{\prime\prime},\,S\!\text{y}\!\text{c}f,\, AUITS^{\prime}]\), where \(SUP^{\prime}\subset\text{SUCI}^{\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}_{\Pi}[\text{UE}^{\prime},\,SN^{\prime\prime},\,HN,\,\text{SUCI}^{\prime},\,RAND,\, AUTN^{\prime},\,S\!\text{y}\!\text{c}f,\, AUITS^{\prime}]\). 3. If \(t\) is a server strand of Definition 3, then \(t\in\text{Serv}_{\Pi}[\text{UE}^{\prime},\,SN,\,HN,\,\text{SUCI}^{\prime},\, SNN,\,RAND,\,AUTN^{\prime},\,(HXRES^{*})^{\prime},\,MACf]\), where \(SUP^{\prime}\subset\text{SUCI}^{\prime}\), \(K^{\prime}\subset AUTN^{\prime}\) and \(K^{\prime}\subset(HXRES^{*})^{\prime}\). According to Theorem 7, the corresponding attack scenarios can be obtained, as shown in Figures 17-19, where the messages between the HN and the authorized SN are protected by their session key. Figure 17: The sixteenth attack scenario of the 5G AKA protocol. Figure 18: The seventeenth attack scenario of the 5G AKA protocol. In Figures 17-19, the green dashed box represents the responder strand of Theorem 8, while the blue dashed boxes represent the initiator strand and the server strand of Theorem 8. 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 17-19, 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\), \((HXRES^{*})^{\prime}\) and \((RES^{*})^{\prime}\), 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 Figures 17 and 19, there are interactions between different cases of the 5G AKA protocol, i.e., cross attacks. They are caused by the penetrators taking advantage of \(Syncf\) and \(MACf\). That is to say, the authentication fails, resulting in a new authentication and key agreement process. 3. In Figure 19, the penetrator replays an encrypted \(MACf\) between the SN and the HN to make authentication failure, i.e., MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process. 4. The initiator strand and the server strand of Theorem 8 may exist in the past run of the protocol, 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 9**.