# 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
: _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}_{III}[UE,\,SN,\,HN,\,SUCI,\,SNN,\,RAND,\,H_{1},\,H_{2},\,MACf]\); (2) \(K^{*}\
otin K_{P}\) and \(K_{SN^{*}HN}\
otin 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\). Then, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{1}[UE^{\prime},\,SN,\,HN,\,SUCI^{\prime},\,SNN,\,RAND,\,AUTN^{\prime},\,(HXRES^{*})^{\prime},\,(RES^{*})^{\prime},\, Result,\,K_{SEAF},\,SUPI^{\prime}]\) and an initiator strand \(s\in\text{Iiti}[UE^{\prime},\,SN,\,HN,\,SUCI^{\prime},\,RAND,\,AUTN^{\prime},\,(RES^{*})^{\prime}]\), where \(SUPI^{\prime}\subset SUCI^{\prime}\), \(SUPI^{\prime}\subset SUCI^{\prime}\), \(K^{\prime}\subset AUTN^{\prime},\,K^{\prime}\subset(HXRES^{*})^{\prime},\,K^{ \prime}\subset(RES^{*})^{\prime},\,K^{\prime}\subset K^{\prime}{}_{SEAF}\) and \(K^{\prime}{}_{SEAF}\) is generated for \(SUPI^{\prime}\). Alternatively, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{II}[UE^{\prime},\,SN,\,HN,\,SUCI^{\prime},\,SNN,\,RAND,\,AUTN^{ \prime},\,(HXRES^{*})^{\prime},\,Syncf,\,AUTS^{\prime}]\) and an initiator strand \(s\in\text{Iiti}_{II}[UE^{\prime},\,SN^{\prime},\,HN,\,SUCI^{\prime},\,RAND,\,AUTN^{ \prime},\,Syncf,\,AUTS^{\prime}]\), where \(SUPI^{\prime}\subset SUCI^{\prime}\), \(SUPI^{\prime}\subset SUCI^{\prime}\), \(K^{\prime}\subset AUTN^{\prime}\), \(K^{\prime}\subset(HXRES^{*})^{\prime}\), \(K^{\prime}\subset AUTS^{\prime}\) and \(SQN_{UE^{\prime}}\subset AUTS^{\prime}\). Alternatively, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{II}[UE^{\prime},\,SN,\,HN,\,SUCI^{\prime},\,SNN,\,RAND,\,AUTN^{ \prime},\,(HXRES^{*})^{\prime},\,MACf]\), where \(SUPI^{\prime}\subset SUCI^{\prime}\), \(SUPI^{\prime}\subset SUCI^{\prime}\), \(K^{\prime}\subset AUTN^{\prime}\), \(K^{\prime}\subset(HXRES^{*})^{\prime}\), \(K^{\prime}\subset AUTS^{\prime}\) and \(SQN_{UE^{\prime}}\subset AUTS^{\prime}\). Figure 19: The eighteenth attack scenario of the 5G AKA protocol. **Proof of Theorem 9. ** It is the same as Theorem 8. \(\square\)  
According to Theorem 9, the corresponding attack scenarios can be obtained as shown in Figures 20-22, where the messages between the HN and the authorized SN are protected by their session key. In Figures 20-22, the green dashed box represents the responder strand of Theorem 9, while the blue dashed boxes represent the initiator strand and the server strand of Theorem 9. 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 20-22, 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}\), which makes 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}_{\mathit{SEAF}}\). That is to say, the authentication fails, resulting in a new authentication and key agreement process. 2. In Figures 20 and 21, there are interactions between different cases of the 5G AKA protocol, i.e., cross attacks. They are caused by the penetrafty taking advantage of \(Syntcf\) and \(MACf\). That is to say, the authentication fails, resulting in a new authentication and key agreement process. 3. In Figures 20-22, the penetrator directly sends \(MACf\) to the SN to make an authentication failure, i.e., MAC failure attacks. That is to say, the authentication fails, resulting in a new authentication and key agreement process. 4.