# 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  
**Theorem 1**. : _Suppose: (1) \(\sum\) is a space for the 5G AKA protocol, and \(\mathcal{C}\) is a bundle containing an initiator strand \(s\in\textsf{Init}_{\textsf{I}}[\)UE, SN, HN, SUCI, \(RAND\), \(AUTN\), \(RES^{*}\)\(]\); (2) \(K\
otin\mathcal{K}_{P}\) and \(K_{SN^{*}HN}\
otin\mathcal{K}_{P}\), where \(SN^{*}\) denotes any authorized SN; (3) RAND is uniquely originating in \(\sum\). Then, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{\textsf{I}}[\)UE, SN\({}^{\prime}\), HN, SUCI\({}^{\prime}\), SNN\({}^{\prime}\), \(RAND\), \(AUTN\), \((HXRES^{*})^{\prime}\), \((RES*)^{\prime}\), Result, \(K^{\prime}_{\textit{SEAF}}\), \(SUPI\)\(]\) and a responder strand \(r\in\text{Resp}_{\textsf{I}}[\)UE\({}^{\prime}\), SN\({}^{\prime}\), HN, SUCI\({}^{\prime}\), SNN\({}^{\prime}\), \(RAND\), AUTN, \((HXRES*)^{\prime}\), \((RES^{*})^{\prime}\), Result, \(K^{\prime}_{\textit{SEAF}}\), \(SUPI^{\prime}\)\(]\), where \(x^{\prime}\subset SUCI^{\prime}\), SNN\({}^{\prime}\subset(HXRES^{*})^{\prime}\), SNN\({}^{\prime}\subset(RES^{*})^{\prime}\), SNN\({}^{\prime}\subset K^{\prime}_{\textit{SEAF}}\), \(SUPI^{\prime}\subset SUCI^{\prime\prime}\) and \(K^{\prime}_{\textit{SEAF}}\) is generated for SUPI\({}^{\prime\prime}\). Alternatively, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{\textsf{III}}[\)UE, SN\({}^{\prime}\), HN, SUCI\({}^{\prime}\), SNN\({}^{\prime}\), \(RAND\), AUTN, \((HXRES^{*})^{\prime}\), \(MACf\)\(]\) and a responder strand \(r\in\text{Resp}_{\textsf{I}}[\)UE\({}^{\prime}\), SN\({}^{\prime}\), HN, SUCI\({}^{\prime}\), SNN\({}^{\prime}\), \(RAND\), AUTN, \((HXRES^{*})^{\prime}\), \((RES^{*})^{\prime}\), Result, \(K^{\prime}_{\textit{SEAF}}\), \(SUPI^{\prime\prime}\)\(]\), \(r\in\text{Resp}_{\textsf{II}}[\)UE\({}^{\prime}\), SN\({}^{\prime}\), HN, SUCI\({}^{\prime}\), SNN\({}^{\prime}\), \(RAND\), AUTN, \((HXRES^{*})^{\prime}\), \(Syncf\), \(H^{\prime\prime}_{4}\)] or \(r\in\text{Resp}_{\textsf{III}}[\)UE\({}^{\prime}\), SN\({}^{\prime}\), HN, SUCI\({}^{\prime}\), SNN\({}^{\prime}\), \(RAND\), AUTN, \((HXRES^{*})^{\prime}\), \(MACf\)\(]\), where \(x^{\prime}\subset SUCI^{\prime}\), SNN\({}^{\prime}\subset(HXRES^{*})^{\prime}\), \(SNN^{\prime}\subset(RES^{*})^{\prime}\), SUPI\({}^{\prime\prime}\subset SUCI^{\prime\prime}\) and \(K^{\prime}_{\textit{SEAF}}\) is generated for SUPI\({}^{\prime\prime}\)._  
Proof of Theorem 1.: By assumptions (2) and (3), \(K\
otin\mathcal{K}_{P}\) and \(RAND\) are uniquely originating in \(\sum\) so \(MAC=f_{1}(K,SQN||RAND||AMF)\subset AUTN\subset term(<s,2>)\) must uniquely originate on a server strand \(t\) according to Definitions 1 to 4. (1) If \(t\) is a server strand of Definition 1, then \(t\in\text{Serv}_{\textsf{I}}[\)UE, SN\({}^{\prime}\), HN, SUCI\({}^{\prime}\), SNN\({}^{\prime}\), \(RAND\), \(AUTN\), \((HXRES^{*})^{\prime}\), \((RES^{*})^{\prime}\), Result, \(K^{\prime}_{\textit{SEAF}}\), \(SUPI\)\(]\), where \(x^{\prime}\subset SUCI^{\prime}\), \(SNN^{\prime}\subset(HXRES^{*})^{\prime}\), \(SNN^{\prime}\subset(RES^{*})^{\prime}\) and \(SNN^{\prime}\subset K^{\prime}_{\textit{SEAF}}\). By assumption (2), \(K_{SN^{\prime}HN}\
otin\mathcal{K}_{P}\), so \(\{(RES^{*})^{\prime}\}_{K_{SN^{\prime}HN}}=term(<t,3>)\) must originate on a responder strand \(r\in\text{Resp}_{\textsf{I}}[\)UE\({}^{\prime}\), SN\({}^{\prime}\), HN, SUCI\({}^{\prime}\), \(SNN^{\prime}\), \(RAND\), \(H^{\prime\prime}_{1}\), \((HXRES^{*})^{\prime}\), \((RES^{*})^{\prime}\)Result, \(K^{\prime\prime}{}_{SEAF}\), \(SUPI^{\prime\prime}\)], where \(SUPI^{\prime\prime}\subset SUCI^{\prime\prime}\) and \(K^{\prime\prime}{}_{SEAF}\) is generated for \(SUPI^{\prime\prime}\). Since \(K_{SN^{\prime},HN}\
otin\mathcal{K}_{P}\), \(\{RAND||H^{\prime\prime}{}_{1}||(HXRES^{*})^{\prime}\}_{K_{SN^{\prime},HN}}= \emph{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\).