# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 4 Our Proposed 5G-AKA' Protocol and Its Security Analysis
### The Initiator's Guarantee of the 5G-AKA' Protocol  
**Theorem 10**. : _Suppose: (1) \(\sum\) is a space for the 5G-AKA' protocol, and \(\mathcal{C}\) is a bundle containing an initiator strand \(s\in\text{Init}_{\text{I}}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,\text{RAND},\, \text{AUTN},\,\text{KEY}^{*}]\); (2) \(K\
otin\mathcal{K}_{P}\) and \(K_{SN,HN}\
otin\mathcal{K}_{P}\); (3) \(x,\,RAND,\,RAND^{\prime}_{\text{SN}}\) is uniquely originating in \(\sum\). Then, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{\text{I}}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,\text{ SNN},\,RAND^{\prime}_{\text{SN}},\,RAND,\,\text{AUTN},\,\text{HXRES}^{*},\,\text{Sev },\,\text{SUPI}]\) and a unique responder strand \(r\in\text{Resp}_{\text{I}}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,\text{ SNN},\,RAND,\,\text{AUTN},\,\text{HXRES}^{*},\,\text{RES}^{*},\,\text{Result},\,\text{K}_{\text{SEAF}},\,\text{SUPI}]\)._  
Proof of Theorem 10.: Since \(BK=KDF(K,x\cdot y\cdot G||SNN)\), \(BK\
otin\mathcal{K}_{P}\) according to assumption (2). Because \(MAC=f_{1}(BK,SQN||RAND||AMF)\) and \(RAND\) is uniquely originating in \(\sum\), \(MAC\subset AUTN\subset term(<s,2>)\) must uniquely originate on a server strand \(t\) according to Definitions 5 to 7. (1) If \(t\) is a server strand of Definition 5, then \(t\in\text{Serv}_{\text{I}}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,\text{ SNN},\,RAND^{\prime}_{\text{SN}},\,RAND,\,\text{AUTN},\,HXRES^{*},\,\text{RES}^{*},\, Result,\,\text{K}_{\text{SEAF}},\,\text{SUPI}]\). By assumptions (2) and (3), \(K_{SN,HN}\
otin\mathcal{K}_{P}\) and \(RAND^{\prime}_{\text{SN}}\) are uniquely originating in \(\sum\), so \(\{RAND^{\prime}_{\text{SN}}||RES^{*}\}_{K_{SN,HN}}=term(<t,3>)\) must originate on a unique responder strand \(r\in\text{Resp}_{\text{I}}[\text{UE}^{*},\,\text{SN},\,HN,\,\text{SUICI}^{ \prime},\,\text{SNN},\,RAND,\,H^{\prime}_{\text{I}},\,HXRES^{*},\,\text{Result},\,K^{ \prime}_{\text{SEAF}},\,\text{SUPPI}^{\prime\prime}]\), where \(\text{SUPPI}^{\prime\prime}\subset\text{SUICI}^{\prime\prime}\). Since \(K_{SN,HN}\
otin\mathcal{K}_{P}\), \(\{RAND^{\prime}_{\text{SN}}||SUPPI^{\prime}||RAND||H^{\prime\prime}_{\text{ I}}||HXRES^{*}\}_{K_{SN,HN}}=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}_{\text{I}}=AUTN\), \(\text{SUPPI}^{\prime\prime}=\text{SUPPI}\) and \(\text{UE}^{\prime\prime}=UE\). Since \(K_{SN,HN}\
otin\mathcal{K}_{P}\), \(\{RAND||Result||K^{\prime\prime}_{\text{SEAF}}||SUPI\}_{K_{SN,HN}}=term(<r,7>)\) must originate on a server strand \(t^{\prime\prime}\). Since \(RAND\) is uniquely originating in \(\sum t^{\prime\prime}=t\), so \(K^{\prime\prime}_{\text{SEAF}}=K_{\text{SEAF}}\). Since \(K_{SN,HN}\
otin\mathcal{K}_{P}\), \(\{RAND^{\prime}_{\text{SN}}||SUICI||SNN\}_{K_{SN,HN}}=term(<t,1>)\) must originate on a responder strand \(r^{\prime}\). Since \(RAND^{\prime}_{\text{SN}}\) is uniquely originating in \(\sum r^{\prime}=r\), so \(SUICI^{\prime\prime}=SUICI\). Hence, \(r\in\text{Resp}_{\text{I}}[\text{UE},\,\text{SN},\,HN,\text{SUICI},\,\text{ SNN},\,RAND^{\prime}_{\text{SN}},\,RAND,\,AUTN,\,HXRES^{*},\,\text{RES}^{*},\,Result,\,K_{\text{SEAF}},\,\text{SUPPI}]\). (2) If \(t\) is a server strand of Definition 6, then \(t\in\text{Serv}_{\text{II}}[\text{UE},\,\text{SN},\,HN,\,\text{SUPI},\, \text{SUICI},\,\text{SNN},\,RAND,\,\text{AUTN},\,HXRES^{*},\,\text{Syncf},\, \text{AUITS}^{\prime}]\), where \(SQN^{\prime}_{\text{UE}}\subset AUTS^{\prime}\). Since \(BK\
otin\mathcal{K}_{P}\), \(MAC-S^{\prime}=f_{1}^{*}(BK,SQN^{\prime}_{\text{UE}}||RAND||AMF_{0})\subset AUTS^{\prime}\subset term(<t,3>)\) must originate on an initiator strand \(s^{\prime}\in\text{Init}_{\text{I}}[\text{UE},\,\text{SN},\,HN,\,\text{ SUPI},\,\text{SUICI},\,RAND,\,AUTN^{\prime},\,\text{Syncf},\,\text{ AUITS}^{\prime}]\), so \(x\) originates on \(term(<s^{\prime},1>)\). By assumptions (1) and (2), \(x\) originates on \(term(<s,1>)\).