# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 3 Formal Verification and Analysis of the 5G AKA Protocol
### The Initiator's Guarantee of the 5G AKA Protocol
Figure 8: The seventh attack scenario of the 5G AKA protocol. Figure 9: The eighth attack scenario of the 5G AKA protocol. According to Figures 6-10, some specific attacks can be found as follows:  
1. \(UE\) cannot find that \(SUCI^{\prime}\) and \(SUCI^{\prime\prime}\) are replayed because \(AUTN\) does not contain the challenge of the UE (i.e., \(x\)), which is included in \(SUCI\). That is to say, the replay attacks on the SN and the HN can be formed, resulting in the energy consumption ion of the SN and the HN. 2. \(UE\) successfully authenticates \(HN\), but does not authenticate \(SN\) because \(AUTN\) does not contain \(SNN\), which means that \(SNN^{\prime}\) is included in \((HXRES^{*})^{\prime}\), \((RES^{*})^{\prime}\) and \(K^{\prime}{}_{SEAF}\), and the principal associated with the responder strand is \(SN^{\prime}\). In [14], the authors also pointed out this security issue. That is to say, the authentication fails, resulting in a new authentication and key agreement process. 3. In Figures 6 and 8-10, 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. 4. In Figures 8 and 9, the penetrator replays an encrypted \(MACf\) between the SN and the HN to make authentication failure. In Figure 10, the penetrator directly sends \(MACf\) to the SN to make authentication failure. They are called MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process. 5. The server strand and the responder strand of Theorem 2 in Figures 6 and 8 only exist in the past run of the protocol according to Theorem 2, i.e., \(RAND||AUTN\) on the initiator strand of Theorem 2 in Figures 6 and 8 is a replayed message and \(SQN\subset AUTN\) is not in the correct range. As a result, the location privacy of the UE can be compromised by identifying \(Syncf\). Further, the server strand and the responder strand of Theorem 2 in Figures 7, 9 and 10 may exist in the past run of the protocol because they do not contain the challenge of the UE (i.e., \(x\)), which is included in \(SUCI\). That is to say, \(RAND||AUTN\) on the UE in Figures 7, 9 and 10 can be a replayed message and \(SQN\subset AUTN\) is not in the correct range. As a result, the location privacy of the UE can be compromised by identifying \(Syncf\). In [14; 15; 18; 24], the authors also exploited this attack. That is to say, the location privacy of the UE can be compromised. **Proof of Theorem 3. ** By the above assumption and Definition 3, \(XMAC\) computed locally is not equal to \(MAC\subset AUTN\subset term(<s,2>)\), so \(MAC\) does not originate on any responder strand and server strand. \(\square\)  
According to Theorem 3, the corresponding attack scenario can be obtained as shown in Figure 11.  
In Figure 11, the green dashed box represents the initiator strand of Theorem 3. According to Figure 11, \(UE\) does not authenticate \(SN\) and \(HN\). The penetrator \(P\) can perform a masquerading attack, where \(RAND||AUTN\) is forged or tampered by \(P\). In the other words, the penetrator can forge or tamper with \(RAND||AUTN\) to make the UE respond to a \"MAC failure\" indication, resulting in authentication failure. This is also called MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process.