# 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
Then, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{\Pi}[\text{UE}^{\prime},\,SN,\,HN,\,\text{SUCI}^{\prime},\, SNN,\,RAND,\,AUTN^{\prime},\,(HXRES^{*})^{\prime},\,(RES^{*})^{\prime},\,Result,\,K_{\text{SEAF}}^{\prime},\,SUP^{\prime}]\) and an initiator strand \(s\in\text{Init}_{\Pi}[\text{UE}^{\prime},\,SN,\,HN,\,\text{SUCI}^{\prime},\,RAND,\, AUTN^{\prime},\,(RES^{*})^{\prime}]\), where \(SUP^{\prime}\subset\text{SUCI}^{\prime},\,SUP^{\prime}\subset\text{SUCI}^{\prime}\), \(K^{\prime}\subset AUTN^{\prime},\,K^{\prime}\subset AUTN^{\prime},\,K^{ \prime}\subset AUTN^{\prime},\,K^{\prime}\subset(HXRES^{*})^{\prime},\,K^{ \prime}\subset(RES^{*})^{\prime},\,K^{\prime}\subset K^{\prime},\,\text{SEAF}\) and \(K^{\prime},\,SEAF\) is generated for \(SUP^{\prime}\). Alternatively, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{\Pi}[\text{UE}^{\prime},\,SN,\,HN,\,\text{SUCI}^{\prime},\, SNN,\,RAND,\,AUTN^{\prime},\,(HXRES^{*})^{\prime},\,S\!\text{y}\!\text{c}f,\, AUITS^{\prime}]\) and an initiator strand \(s\in\text{Init}_{\Pi}[\text{UE}^{\prime},\,SN^{\prime},\,HN,\,\text{SUCI}^{\prime},\,RAND,\, AUTN^{\prime},\,S\!\text{y}\!\text{c}f,\,AUITS^{\prime}]\), where \(SUP^{\prime}\subset\text{SUCI}^{\prime},\,SUP^{\prime}\subset\text{SUCI}^{\prime},\,K^{ \prime}\subset AUTN^{\prime},\,K^{\prime}\subset(HXRES^{*})^{\prime},\,K^{ \prime}\subset AUTS^{\prime}\) and \(SQN_{\text{UE}^{\prime}}\subset AUTS^{\prime}\). Alternatively, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{\Pi}[\text{UE}^{\prime},\,SN,\,HN,\,\text{SUCI}^{\prime},\, SNN,\,RAND,\,AUTN^{\prime},\,(HXRES^{*})^{\prime},\,MACf]\), where \(SUP^{\prime}\subset\text{SUCI}^{\prime},\,K^{\prime}\subset AUTN^{\prime}\) and \(K^{\prime}\subset(HXRES^{*})^{\prime}\). Proof of Theorem 7.: By assumptions (2) and (3), \(K_{\text{SN},HN}\
otin\mathcal{K}_{p}\) and \(RAND\) are uniquely originating in \(\sum\) so \(\{RAND||H_{1}||H_{2}\}_{K_{\text{SN},HN}}=term(<r,3>)\) 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}_{1}[\text{UE}^{\prime},\,SN,\,HN,\,\text{SUCI}^{\prime},\, SNN,\,RAND,\,AUTN^{\prime},\,(HXRES^{*})^{\prime},\,Result,\,K^{\prime},\,SUP^{\prime}]\), where \(SUP^{\prime}\subset\text{SUCI}^{\prime},\,K^{\prime}\subset AUTN^{\prime},\,K^{ \prime}\subset(HXRES^{*})^{\prime},\,K^{\prime}\subset(RES^{*})^{\prime},\,K^{ \prime}\subset(RES^{*})^{\prime},\,K^{\prime}\subset K^{\prime}\,S\!\text{e}f \) and \(K^{\prime}\) is generated for \(SUP^{\prime}\). By assumption (2), \(K^{\prime}\
otin\mathcal{K}_{p}\). Since \(CK^{\prime}=f_{3}(K^{\prime},RAND)\) and \(IK^{\prime}=f_{4}(K^{\prime},RAND)\), \(CK^{\prime}\
otin\mathcal{K}_{p}\) and \(IK^{\prime}\
otin\mathcal{K}_{p}\), so \(CK^{\prime}||IK^{\prime}\
otin\mathcal{K}_{p}\). Hence, \((RES^{*})^{\prime}=KDF(CK^{\prime}||IK^{\prime},\,SNN||RAND|RES^{\prime})\subset term(<t,3>)\) must originate on an initiator strand \(s\in\text{Init}_{\Pi}[\text{UE}^{\prime},\,SN,\,HN,\,\text{SUCI}^{\prime},\,RAND, \,AUTN^{\prime},\,(RES^{*})^{\prime}]\), where \(SUIP^{\prime}\subset\text{SUCI}^{\prime}\) and \(SQN^{\prime\prime}\subset AUTN^{\prime\prime}\). Since \(K^{\prime}\
otin\mathcal{K}_{p}\), \(MAC^{\prime\prime}=f_{1}(K^{\prime},SQN^{\prime\prime}\)\(||RAND|AMF)\subset AUTN^{\prime\prime}\). \(term(<s,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^{\prime}\). Hence, \(s\in\text{Init}_{\Pi}[\text{UE}^{\prime},\,SN,\,HN,\,\text{SUCI}^{\prime},\,RAND, \,AUTN^{\prime},\,(RES^{*})^{\prime}]\). 2.