# 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
If \(t\) is a server strand of Definition 2, then \(t\in\mathrm{Serv}_{\Pi}[UE,\,SN^{\prime},\,HN,\,SUCI^{\prime},\,SNN^{\prime},\,RAND,\,AUTN,\,(HXRES^{*})^{\prime}, \,Syncf,\,AUTS^{\prime}]\), where \(x^{\prime}\subset SUCI^{\prime},\,SNN^{\prime}\subset(HXRES^{*})^{\prime}\) and \(SQN^{\prime}{}_{UE}\subset AUTS^{\prime}\). By assumption (2), \(K_{SN^{\prime},HN}\
ot\in\mathcal{K}_{P}\), so \(\{Syncf||RAND||AUTS^{\prime}\}_{K_{SN^{\prime},HN}}=\mathit{term}(<t,3>)\) must originate on a responder strand \(r\in\mathrm{Resp}_{\Pi}[UE^{\prime\prime},\,SN^{\prime},\,HN,\,SUCI^{\prime \prime},\,SNN^{\prime},\,RAND,\,H^{\prime\prime}{}_{1},\,H^{\prime\prime}{}_ {2},\,Syncf,\,AUTS^{\prime}]\), where \(SUPI^{\prime\prime}\subset SUCI^{\prime\prime}\). Since \(K_{SN^{\prime},HN}\
ot\in\mathcal{K}_{P}\), \(\{RAND||H^{\prime\prime}||H^{\prime\prime}{}_{2}\}_{K_{SN^{\prime},HN}}= \mathit{term}(<r,3>)\) must originate on a server strand \(t^{\prime}\). Since \(RAND\) is uniquely originating in \(\sum\), \(t^{\prime}=t\), so \(H^{\prime\prime}{}_{1}=AUTN\) and \(H^{\prime\prime}{}_{2}=(HXRES^{*})^{\prime}\). Hence, \(r\in\mathrm{Resp}_{\Pi}[UE^{\prime\prime},\,SN^{\prime},\,HN,\,SUCI^{\prime},\, SNN^{\prime},\,RAND,\,AUTN,\,(HXRES^{*})^{\prime},\,Syncf,\,AUTS^{\prime}]\). 3. If \(t\) is a server strand of Definition 3, then \(t\in\mathrm{Serv}_{\Pi}[UE,\,SN^{\prime},\,HN,\,SUCI^{\prime},\,SNN^{\prime},\,RAND,\,AUTN,\,(HXRES^{*})^{\prime},\,MACf]\), where \(x^{\prime}\subset SUCI^{\prime}\) and \(SNN^{\prime}\subset(HXRES^{*})^{\prime}\). Since \(RAND\) is uniquely originating in \(\sum\), \(RAND\) originates at \(n_{0}=<t,2>\), where \(v_{0}=\mathit{term}(<t,2>)=\{RAND||AUTN||(HXRES^{*})^{\prime}\}_{K_{SN^{ \prime},HN}}\). Let \(S=\{n\in\mathcal{C}:RAND\subset term(n)\wedge v_{0}\mathit{term}(n)\}\). Since \(\mathit{term}(<s,2>)=RAND||AUTN\in\mathcal{C}\), \(S\) is non-empty. Hence, \(S\) has at least one \(\leq\)-minimal element \(n_{2}\) and the sign of \(n_{2}\) is positive. \(n_{2}\) does not lie on a penetrator strand but must lie on a regular strand instead (Lemma 5.4 in [29]). By inspection, \(n_{1}\) precedes \(n_{2}\) on the regular strand and \(\mathit{term}(n_{1})=v_{0}\), and the regular strand containing \(n_{1}\) and \(n_{2}\) is a responder strand \(r\). If \(r\) is a responder strand of Definition 1, then \(r\in\mathrm{Resp}_{1}[UE^{\prime\prime},\,SN^{\prime},\,HN,\,SUCI^{\prime\prime},\, SNN^{\prime},\,RAND,\,AUTN,\,(HXRES^{*})^{\prime},\,(RES^{*})^{\prime},\,Result,\,K^{\prime}{}_{ \mathit{SEAF}},\,SUPI^{\prime\prime}]\), where \(\mathit{SNN^{\prime}}\subset(RES^{*})^{\prime}\), \(SUPI^{\prime\prime}\subset SUCI^{\prime\prime}\) and \(K^{\prime\prime}{}_{\mathit{SEAF}}\) is generated for \(SUPI^{\prime\prime}\). From the above, it is possible that \(r\) is a responder strand of Definition 1 because it is possible from \(SQN_{UE}<SQN\) to \(SQN_{UE}\geq SQN\), and both \(r\) and \(t\) must exist in the past run of the protocol. If \(r\) is a responder strand of Definition 2, then \(r\in\mathrm{Resp}_{\Pi}[UE^{\prime\prime},\,SN^{\prime},\,HN,\,SUCI^{\prime\prime},\, SNN^{\prime},\,RAND,\,AUTN,\,(HXRES^{*})^{\prime},\,Syncf,\,H^{\prime\prime}{}_{4}]\). If \(r\) is a responder strand of Definition 3, then \(r\in\mathrm{Resp}_{\Pi}[UE^{\prime\prime},\,SN^{\prime},\,HN,\,SUCI^{\prime\prime}, \,SNN^{\prime},\,RAND,\,AUTN,\,(HXRES^{*})^{\prime},\,MACf]\). \(\Box\)  
According to Theorem 2, the corresponding attack scenarios can be obtained as shown in Figures 6-10, where the messages between the HN and the authorized SN are protected by their session key. In Figures 6-10, the green dashed box represents the initiator strand of Theorem 2, while the blue dashed boxes represent the server strand and the responder strand of Theorem 2. The fields marked in red on the server strand and the responder strand are some fields that cannot be agreed with the UE, which are caused by MitM attacks. Figure 6: The fifth attack scenario of the 5G AKA protocol. Figure 7: The sixth attack scenario of the 5G AKA protocol.