# 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
(2) If \(t\) is a server strand of Definition 6, then \(t\in\text{Serv}_{l}[\text{UE},\,\text{SN},\,HN,\text{SUPI},\,\text{SUICI}^{ \prime},\,\text{SNN},\,RAND_{\text{SN}},\,RAND,\,AUTN^{\prime},\,(HXRES^{*})^{ \prime},\,Syncf,\,AUTS^{\prime}]\), where \(\text{SUPI}\subset\text{SUICI}^{\prime}\), \(x^{\prime}\subset AUTN^{\prime}\), \(x^{\prime}\subset(HXRES^{*})^{\prime}\) and \(x^{\prime}\subset AUITS^{\prime}\). Since \(K_{\text{SN},HN}\
otin\mathcal{K}_{P}\), \(\{RAND_{\text{SN}}||Syncf||RAND||AUTS^{\prime}\}_{K_{\text{SN},HN}}=\text{term}(<t,3>)\) must originate on a responder strand \(r^{\prime}\in\text{Resp}_{l}[\text{UE}^{\prime},\,\text{SN},\,HN,\,\text{SUPI}^{ \prime\prime},\,SUICI^{\prime\prime},\,\text{SNN},\,RAND_{\text{SN}},\,RAND_{ \text{SN}},\,H^{\prime\prime},\,H^{\prime\prime},\,Syncf,\,AUTS^{\prime}]\), so \(RAND_{\text{SN}}\) originates on \(\text{term}(<r^{\prime},2>)\). By assumptions (1) and (2), \(RAND_{\text{SN}}\) originates on \(\text{term}(<r,2>)\). Since \(RAND_{\text{SN}}\) is uniquely originating in \(\sum\)\(r^{\prime}=r\). However, \(r^{\prime}\in\text{Resp}_{l}\) and \(r\in\text{Resp}_{l}\), \(r^{\prime}\
eq r\). Hence, \(t\) is not a server strand of Definition 6. \(\square\)  
**Theorem 15**. : _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{SUPI},\,\text{SUICI},\, \text{SNN},\,RAND_{\text{SN}},\,RAND,\,H_{1},\,H_{2},\,Syncf,\,H_{4}]\); (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{SUPI},\,\text{SUICI},\, SNN,\,RAND_{\text{SN}},\,RAND_{\text{SN}},\,AUTN,\,HXRES^{*},\,Syncf,\,AUTS]\) and a unique initiator strand \(s\in\text{Init}_{l}[\text{UE},\,\text{SN},\,HN,\text{SUICI},\,RAND,\,AUTN,\, Syncf,\,AUTS]\)._  
Proof of Theorem 15.: By assumptions (2) and (3), \(K_{\text{SN},HN}\
otin\mathcal{K}_{P}\) and \(RAND\) and 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},\,RAND_{\text{SN}},\,RAND,\,AUTN^{\prime},\,\(SUPI\subset SUCI^{\prime}\), \(x^{\prime}\subset 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 \(SUPI\). Since \(K_{SN,HN}\
otin\mathcal{K}_{P}\), \(\{RAND_{SN}||(RES^{*})^{\prime}\}_{K_{SN,HN}}\)\(=term(<t,3>)\) must originate on a unique responder strand \(r^{\prime}\in\text{Resp}_{\text{I}}\{UE^{\prime}\), \(SN\), \(HN\), \(SUCI^{\prime}\), \(SNN\), \(RAND_{SN}\), \(RAND\), \(H^{\prime\prime}\), \((HXRES^{*})^{\prime}\), \((RES^{*})^{\prime}\), \(Result\), \(K^{\prime\prime}_{SEAF}\), \(SUPI^{\prime\prime}\)), so \(RAND_{SN}\) originates on \(term(<r^{\prime},2>)\). By assumptions (1) and (2), \(RAND_{SN}\) originates on \(term(<r,2>)\). Since \(RAND_{SN}\) is uniquely originating in \(\sum\), \(r^{\prime}=r\). However, \(r^{\prime}\in\text{Resp}_{\text{I}}\) and \(r\in\text{Resp}_{\text{II}}\), \(r^{\prime}\
eq r\). Hence, \(t\) is not a server strand of Definition 5. 2. If \(t\) is a server strand of Definition 6, then \(t\in\text{Serv}_{\text{II}}[UE\), \(SN\), \(HN\), \(SUPI\), \(SUCI^{\prime}\), \(SNN\), \(RAND_{SN}\), \(RAND\), \(AUTN^{\prime}\), \((HXRES^{*})^{\prime}\), \(Syntcf\), \(AUTS^{\prime}\)], where \(SUPI\subset SUCI^{\prime}\), \(x^{\prime}\subset AUTN^{\prime}\), \(x^{\prime}\subset(HXRES^{*})^{\prime}\) and \(x^{\prime}\subset AUTS^{\prime}\).