# 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
Then, \(\mathcal{C}\) contains a unique server strand \(t\in\mathit{Serv}_{\parallel}\{\mathit{UE},\,\mathit{SN}^{\prime},\,\mathit{HN},\, \mathit{SUCI}^{\prime},\,\mathit{SNN}^{\prime},\,\mathit{RAND},\,\mathit{AUTN},\, \mathit{(HXRES^{*})^{\prime}},\,\mathit{(RES^{*})^{\prime}},\,\mathit{Result},\, \mathit{K^{\prime}SEAF},\,\mathit{SUPI}\}\) and a responder strand \(r\in\mathit{Resp}_{\parallel}\{\mathit{UE}^{\prime\prime},\,\mathit{SN}^{ \prime},\,\mathit{HN},\,\mathit{SUCI}^{\prime\prime},\,\mathit{SNN}^{\prime}, \,\mathit{RAND},\,\mathit{AUTN},\,\mathit{(HXRES^{*})^{\prime}},\,\mathit{( RES^{*})^{\prime}},\,\mathit{Result},\, \mathit{K^{\prime\prime}SEAF},\,\mathit{SUPI}^{\prime\prime}\}\), and both \(t\) and \(r\) must exist in the past run of the protocol, where \(x^{\prime}\subset\mathit{SUCI}^{\prime}\), \(\mathit{SNN}^{\prime}\subset(HXRES^{*})^{\prime}\), \(\mathit{SNN}^{\prime}\subset(RES^{*})^{\prime}\), \(\mathit{SNN}^{\prime}\subset K^{\prime}SEAF\), \(\mathit{SUPI}^{\prime\prime}\subset\mathit{SUCI}^{\prime\prime}\) and \(K^{\prime\prime}\)'\(\mathit{SEAF}\) is generated for \(\mathit{SUPI}^{\prime\prime}\). Alternatively, \(\mathcal{C}\) contains a unique server strand \(t\in\mathit{Serv}_{\parallel}\{\mathit{UE},\,\mathit{SN}^{\prime},\,\mathit{HN},\, \mathit{SUCI}^{\prime},\,\mathit{SNN}^{\prime},\,\mathit{RAND},\,\mathit{AUTN},\, \mathit{(HXRES^{*})^{\prime}},\,\mathit{Syncf},\,\mathit{AUTS}^{\prime}\}\) and a responder strand \(r\in\mathit{Resp}_{\parallel}\{\mathit{UE}^{\prime\prime},\,\mathit{SNN}^{ \prime},\,\mathit{HN},\,\mathit{SUCI}^{\prime\prime},\,\mathit{SNN}^{\prime}, \,\mathit{RAND},\,\mathit{AUTN},\,\mathit{(HXRES^{*})^{\prime}},\,\mathit{ Syncf},\,\mathit{AUTS}^{\prime}\}\), where \(\mathit{x}^{\prime}\subset\mathit{SUCI}^{\prime}\), \(\mathit{SNN}^{\prime}\subset(HXRES^{*})^{\prime}\), \(\mathit{SQN}^{\prime}_{\mathit{UE}}\subset\mathit{AUTS}^{\prime}\) and \(\mathit{SUPI}^{\prime\prime}\subset\mathit{SUCI}^{\prime\prime}\). Alternatively, \(\mathcal{C}\) contains a unique server strand \(t\in\mathit{Serv}_{\parallel}\{\mathit{UE},\,\mathit{SN}^{\prime},\,\mathit{HN},\, \mathit{SUCI}^{\prime},\,\mathit{SNN}^{\prime},\,\mathit{RAND},\,\mathit{AUTN},\, \mathit{(HXRES^{*})^{\prime}},\,\mathit{MACF}\}\) and a responder strand \(r\in\mathit{Resp}_{\parallel}\{\mathit{UE}^{\prime},\,\mathit{SN}^{\prime},\, \mathit{HN},\,\mathit{SUCI}^{\prime\prime},\,\mathit{SNN}^{\prime},\, \mathit{RAND},\,\mathit{AUTN},\,\mathit{(HXRES^{*})^{\prime}},\,\mathit{ (RES^{*})^{\prime}},\,\mathit{Result},\,K^{\prime}SEAF,\,\mathit{SUPI}^{ \prime}\}\), \(r\in\mathit{Resp}_{\parallel}\{\mathit{UE}^{\prime},\,\mathit{SNN}^{\prime}, \,\mathit{HN},\,\mathit{SUCI}^{\prime\prime},\,\mathit{SNN}^{\prime},\, \mathit{RAND},\,\mathit{AUTN},\,\mathit{(HXRES^{*})^{\prime}},\,\mathit{ Syncf},\,\mathit{H}^{\prime}4\}\) or \(r\in\mathit{Resp}_{\parallel}\{\mathit{UE}^{\prime},\,\mathit{SNN}^{\prime}, \,\mathit{HN},\,\mathit{SUCI}^{\prime\prime},\,\mathit{SNN}^{\prime},\, \mathit{RAND},\,\mathit{AUTN},\,\mathit{(HXRES^{*})^{\prime}},\,\mathit{MACF}\}\), where \(x^{\prime}\subset\mathit{SUCI}^{\prime}\), \(\mathit{SUI}^{\prime\prime}\subset\mathit{SUCI}^{\prime\prime}\) and \(K^{\prime}\)'\(\mathit{SEAF}\) is generated for \(\mathit{SUPI}^{\prime\prime}\), and both \(t\) and \(r\) must exist in the past run of the protocol when \(r\in\mathit{Resp}_{\parallel}\{\mathit{UE}^{\prime},\,\mathit{SN}^{\prime},\, \mathit{HN},\,\mathit{SUCI}^{\prime},\,\mathit{SNN}^{\prime},\,\mathit{RAND},\, \mathit{AUTN},\,\mathit{(HXRES^{*})^{\prime}},\mathit{(RES^{*})^{\prime}},\, \mathit{Result},K^{\prime\prime}SEAF,\,\mathit{SUPI}^{\prime\prime}\}\)._  
Proof of Theorem 2.: By assumptions (2) and (3), \(K\
otin\mathcal{K}_{p}\) and \(RAND\) are uniquely originating in \(\sum\), so \(\mathit{MAC}=f_{1}(K,\mathit{SQN}||RAND||AMF)\subset AUTN\subset term(<s,2>)\) must uniquely originate on a server strand \(t\) according to Definitions 1 to 4.