# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 4 Our Proposed 5G-AKA' Protocol and Its Security Analysis
### The Responder's Guarantee of the 5G-AKA' Protocol  
**Theorem 14**. : _Suppose: (1) \(\sum\) is a space for the 5G-AKA' protocol, and \(\mathcal{C}\) is a bundle containing a responder strand \(r\in\text{Resp}_{l}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,\text{SNN},\, \text{RAND}_{\text{SN}},\,\text{RAND},\,H_{1},\,\text{H}_{2},\,H_{3},\,\text{ Result},\,K_{SEAF},\,\text{SUIPI}]\); (2) \(K\
otin\mathcal{K}_{P}\) and \(K_{\text{SN},HN}\
otin\mathcal{K}_{P}\); (3) \(x\), \(RAND\), \(RAND_{\text{SN}}\) is uniquely originating in \(\sum\). Then, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{l}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,\text{SNN},\, \text{RAND}_{\text{SN}},\,\text{RAND},\,\text{AUTN},\,HXRES^{*},\,\text{RES}^{*}, \,Result,\,K_{SEAF},\,\text{SUPI}]\) and a unique initiator strand \(s\in\text{Init}_{l}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,RAND,\,AUTN,\, RES*]\)._  
Proof of Theorem 14.: By assumptions (2) and (3), \(K_{\text{SN},HN}\
otin\mathcal{K}_{P}\) and \(RAND\) are uniquely originating in \(\sum\), so \(\{RAND_{\text{SN}}||SUPI||RAND||H_{1}||H_{2}\}_{K_{\text{SN},HN}}=\text{term}(<r,3>)\) 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}_{l}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI}^{\prime},\,\text{ SNN},\,\text{RAND}_{\text{SN}},\,RAND,\,\text{AUTN}^{\prime},\,(HXRES^{*})^{\prime},\,(RES^{*})^{\prime},\,Result,\,K^{\prime}_{SEAF},\, \text{SUPI}]\), where \(\text{SUPI}\subset\text{SUICI}^{\prime}\), \(x^{\prime}\subset\text{AUTN}^{\prime}\), \(x^{\prime}\subset(HXRES^{*})^{\prime}\), \(x^{\prime}\subset(RES^{*})^{\prime}\), \(x^{\prime}\subset K^{\prime}_{SEAF}\) and \(K^{\prime}_{SEAF}\) is generated for \(\text{SUPI}\). Since \(K_{\text{SN},HN}\
otin\mathcal{K}_{P}\), \(\{RAND||Result||K_{SEAF}\)\(||SUPI\}_{K_{\text{SN},HN}}=\text{term}(<r,7>)\) must originate on a server strand \(t^{\prime}\). Since \(RAND\) is uniquely originating in \(\sum\)\(t^{\prime}=t\), so \(K^{\prime}_{SEAF}=K_{SEAF}\). Since \(K_{\text{SN},HN}\
otin\mathcal{K}_{P}\), \(\{RAND_{\text{SN}}||SUICI^{\prime}||SNN\}_{K_{\text{SN},HN}}=\text{term}(<t,1>)\) must originate on a responder strand \(t^{\prime}\). Since \(RAND_{\text{SN}}\) is uniquely originating in \(\sum\)\(t^{\prime}=r\), so \(SUICI^{\prime}=SUICI\) and \(x^{\prime}=x\) according to assumption (1). As a result, \(AUTN^{\prime}=AUTN\), \((HXRES^{*})^{\prime}=HXRES^{*}\) and \((RES^{*})^{\prime}=RES^{*}\). Hence, \(t\in\text{Serv}_{l}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,\text{SNN}, \,RAND_{\text{SN}},\,RAND,\,AUTN,\,HXRES^{*},\,RES^{*},\,Result,\,K_{SEAF},\, \text{SUPI}]\). Since \(BK=\text{K}DF(K,x\cdot y\cdot G||SNN)\), \(BK\
otin\mathcal{K}_{P}\) according to assumption (2). Because \(CK=f_{3}(BK,RAND)\) and \(IK=f_{4}(BK,RAND)\), \(CK\
otin\mathcal{K}_{P}\) and \(IK\
otin\mathcal{K}_{P}\), so \(CK||IK\
otin\mathcal{K}_{P}\). By assumption (3), \(x\) is uniquely originating in \(\sum\), so \(RES^{*}=KDF(CK||IK,\text{SNN}||RAND||RES)\subset\text{term}(<t,3>)\) must originate on a unique initiator strand \(s\in\text{Init}_{l}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,RAND,\,AUTN^{ \prime},\,RES^{*}]\), where \(\text{SQN}^{\prime\prime}\subset AUTN^{\prime}\). Since \(BK\
otin\mathcal{K}_{P}\), \(MAC^{*}=f_{1}(BK,\text{SQN}^{*}||RAND||AMF)\)\(\subset AUTN^{\prime\prime}\subset\text{term}(<s,2>)\) must originate on a server strand \(t^{\prime}\). Since \(RAND\) is uniquely originating in \(\sum\)\(t^{\prime\prime}=t\), so \(\text{SQN}^{*}=\text{SQN}\) and \(AUTN^{\prime\prime}=AUTN\). Hence, \(s\in\text{Init}_{l}[\text{UE},\,\text{SN},\,HN,\text{SUICI},\,RAND,\,AUTN,\, RES^{*}]\).