# 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
Since \(x\) is uniquely originating in \(\sum s^{\prime}=s\). However, \(s^{\prime}\in\text{Init}_{\text{I}}\) and \(s\in\text{Init}_{\text{I}},\,s^{\prime}\
eq s\). Hence, \(t\) is not a server strand of Definition 6. **Theorem 11**. : _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},\,RAND,\, \text{AUTN},\,\text{Syncf},\,\text{AUITS}^{\prime}]\); (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{II}}[\text{UE},\,\text{SN},\,HN,\,\text{SUICI},\,\text{ SNN},\,RAND^{\prime}_{\text{SN}},\,RAND,\,\text{AUTN},\,HXRES^{*},\,\text{Syncf},\, \text{AUITS}]\) and a unique responder strand \(r\in\text{Resp}_{\text{II}}[\text{UE},\,\text{SN},\,HN,\,\text{SUPI},\, \text{SUICI},\,\text{ SNN},\,RAND^{\prime}_{\text{SN}},\,RAND,\,\text{AUTN},\,HXRES^{*},\, \text{Syncf},\,\text{AUITS}^{\prime}]\)._  
Proof of Theorem 11.: 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\) are 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{SUPPI}]\). Since \(BK\
otin\mathcal{K}_{P}\), \(CK=f_{3}(BK,RAND)\
otin\mathcal{K}_{P}\) and \(IK=f_{4}(BK,RAND)\
otin\mathcal{K}_{P}\), so \(CK||IK\
otin\mathcal{K}_{P}\). Hence, \(RES^{*}=KDF(CK||IK,SNN||RAND||RES)\subset term(<t,3>)\) must originate on an initiator strand \(s^{\prime}\in\text{Init}_{\text{I}}[\text{UE},\,\text{SN},HN,\,\text{SUICI},\,RAND,\, \text{AUTN}^{\prime},\,RES^{*}]\), so \(x\) originates on \(term(<s^{\prime},1>)\). By assumptions (1) and (2), \(x\) originates on \(term(<s,1>)\). Since \(x\) is uniquely originating in \(\sum s^{\prime}=s\). However, \(s^{\prime}\in\mathrm{Init}_{1}\) and \(s\in\mathrm{Init}_{1},s^{\prime}\
eq s\). Hence, \(t\) is not a server strand of Definition 5. 2. If \(t\) is a server strand of Definition 6, then \(t\in\mathrm{Serv}_{\mathrm{II}}[\mathit{UE},\mathit{SN},\mathit{HN},\mathit{ SUPI},\mathit{SUCI},\mathit{SNN},\mathit{RAND}^{\prime}{}_{\mathit{SN}},\mathit{RAND}, \mathit{AUTN},\mathit{HXRES}^{*},\mathit{Syncf},\mathit{AUTN}^{\prime}]\), where \(\mathit{SQN}^{\prime}{}_{\mathit{UE}}\subset\mathit{AUTN}^{\prime}\). Since \(BK\
otin\mathcal{K}_{P}\), \(\mathit{MAC}-S^{\prime}=f_{1}^{*}(BK,\mathit{SQN}^{\prime}{}_{\mathit{UE}} \big{|}\big{|}\mathit{RAND}\big{|}\big{|}\mathit{AMF}_{0})\subset\mathit{AUTN }^{\prime}\subset term(<t,3>)\) must originate on an initiator strand \(s^{\prime}\). Since \(x\) is uniquely originating in \(\sum s^{\prime}=s\), so \(\mathit{SQN}^{\prime}{}_{\mathit{UE}}=\mathit{SQN}{}_{\mathit{UE}}\) and \(\mathit{AUTS}^{\prime}=\mathit{AUTS}\). Hence, \(t\in\mathrm{Serv}_{\mathrm{II}}[\mathit{UE},\mathit{SN},\mathit{HN},\mathit{ SUPI},\mathit{SUCI},\mathit{SNN},\mathit{RAND}^{\prime}{}_{\mathit{SN}},\mathit{RAND}, \mathit{AUTN},\mathit{HXRES}^{*},\mathit{Syncf},\mathit{AUTN}]\).