# 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
Hence, \(r\in\text{Resp}[UE,\ SN^{\prime},\ HN,\ SUCI^{\prime\prime},\ SNN^{\prime},\ RAND,\ AUTN,\)\((HXRES^{*})^{\prime},\)\((RES^{*})^{\prime},\)\(Result,\)\(K^{\prime\prime}{}_{SEAF},\)\(SUPI^{\prime\prime}\). 2. If \(t\) is a server strand of Definition 2, then \(t\in\text{Serv}_{\Pi}[UE,\ SN^{\prime},\ HN,\ SUCI^{\prime\prime},\ SNN^{\prime},\)\(RAND,\ AUTN,\)\((HXRES^{*})^{\prime},\)\(\emph{Syntc},\)\(\emph{AUTS}^{\prime}]\), where \(x^{\prime}\subset SUCI^{\prime},\ SNN^{\prime}\subset(HXRES^{*})^{\prime}\) and \(SQN^{\prime}{}_{UE}\subset AUTS^{\prime}\). By assumption (2), \(K\
otin\mathcal{K}_{P}\), so \((MAC-S)^{\prime}=f_{1}(K,SQN^{\prime}{}_{UE}||RAND||AMF_{0})\)\(\subset AUTS^{\prime}\subset\emph{term}(<t,3>)\) must originate on an initiator strand \(s^{\prime}\in\text{Initi}_{\Pi}[UE,\ SN^{\prime\prime},\ HN,\ SUCI^{\prime\prime},\ RAND,\ AUTN^{\prime\prime},\)\(\emph{Syntc},\)\(\emph{AUTS}^{\prime}]\), where \(\emph{AUTS}^{\prime\prime}=SQN^{\prime\prime}\oplus AK||AMF||MAC^{\prime\prime}\) and \(MAC^{\prime\prime}=f_{1}(K,SQN^{\prime\prime}||RAND||AMF)\). Since \(K\
otin\mathcal{K}_{P}\), \(MAC^{\prime\prime}\subset AUTN^{\prime\prime}\subset\emph{term}(<s^{\prime},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\). By assumption (1) and Definition 1, \(SQN_{UE}<SQN\) on \(s\). However, \(SQN_{UE}\geq SQN\) on \(s^{\prime}\) according to Definition 2. Therefore, \(s\) and \(s^{\prime}\) cannot be in the same run of the protocol, so \(s^{\prime}\) must exist in the past run of the protocol. However, it is impossible from \(SQN_{UE}\geq SQN\) to \(SQN_{UE}<SQN\) because \(SQN_{UE}\) increases. That is to say, it is impossible that \(s^{\prime}\) exists in the past run of the protocol and \(s\) exists in the current run of the protocol. Hence, \(t\) is not a server strand of Definition 2. 3. If \(t\) is a server strand of Definition 3, then \(t\in\text{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}=\emph{term}(<t,2>)=\{RAND||AUTN||(HXRES^{*})^{\prime}\}_{K_{SN^{\prime},HN}}\). Let \(S=\{n\in\mathcal{C}:RAND\subset\emph{term}(n)\wedge v_{0}\emph{term}(n)\}\). Since \(\emph{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 preattor strand but must lie on a regular strand and (Lemma 5.4 in [29]). By inspection, \(n_{1}\) precedes \(n_{2}\) on the regular strand and \(\emph{term}(n_{1})=v_{0}\), and the regular strand containing \(n_{1}\) and \(n_{2}\) is a responder strand \(r\). If \(t\) is a responder strand of Definition 1, then \(r\in\text{Resp}_{\Pi}[UE^{\prime},\ SN^{\prime},\)\(HN,\ SUCI^{\prime\prime},\)\(SNN^{\prime},\)\(RAND,\ AUTN,\)\((HXRES^{*})^{\prime},\)\((RES^{*})^{\prime},\)\(Result,\)\(K^{\prime\prime}{}_{SEAF},\)\(SUPI^{\prime\prime}\), where \(SNN^{\prime}\subset(RES^{*})^{\prime}\), \(SUPI^{\prime\prime}\subset SUCI^{\prime\prime}\) and \(K^{\prime\prime}{}_{SEAF}\) is generated for \(SUPI^{\prime\prime}\). If \(r\) is a responder strand of Definition 2, then \(r\in\text{Resp}_{\Pi}[UE^{\prime},\ SN^{\prime},\ HN,\ SUCI^{\prime\prime},\ SNN^{\prime},\)\(RAND,\ AUTN,\)\((HXRES^{*})^{\prime},\)\(\emph{Syntc}f,\)\(H^{\prime\prime}{}_{4}]\). If \(r\) is a responder strand of Definition 3, then \(r\in\text{Resp}_{\Pi}[UE^{\prime},\ SN^{\prime},\ HN,\ SUCI^{\prime\prime},\ SNN^{\prime},\)\(RAND,\ AUTN,\)\((HXRES^{*})^{\prime},\)\(MACf]\). \(\Box\)  
According to Theorem 1, the corresponding attack scenarios can be obtained as shown in Figures 2-5, where the messages between the HN and the authorized SN are protected by their session key.