# 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  
**Theorem 7**. : _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},\) SN, \(HN,\) SUCI, \(SNN\), \(RAND\), \(H_{1}\), \(H_{2}\), \(H_{3}\). Result, \(K_{SEAF}\), SUPI\(]\); (2) \(K^{*}\
otin\mathcal{K}_{P}\) and \(K_{SN^{*}HN}\
otin\mathcal{K}_{P}\), where \(SN^{*}\) denotes any authorized SN and \(K^{*}\) denotes a pre-shared key between \(HN\) and any authorized UE; (3) \(RAND\) is uniquely originating in \(\sum\). Then, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{l}[\text{UE}^{\prime},\) SN, \(HN,\) SUCI\({}^{\prime},\) SNN, \(RAND\), \(AUTN^{\prime},\)\((HXRES^{*})^{\prime},\)\((RES^{*})^{\prime},\) Result, \(K^{\prime}_{SEAF},\)\(SUPI^{\prime}]\) and an initiator strand \(s\in\text{Init}_{l}[\text{UE}^{\prime},\) SN, \(HN,\) SUCI\({}^{\prime},\)\(RAND\), \(AUTN^{\prime},\)\((RES^{*})^{\prime}\)\(]\), where \(SUPI^{\prime}\subset SUCI^{\prime}\), \(SUPI^{\prime}\subset SUCI^{\prime}\), \(K^{\prime}\subset AUTN^{\prime}\), \(K^{\prime}\subset(HXRES^{*})^{\prime}\), \(K^{\prime}\subset(RES^{*})^{\prime}\), \(K^{\prime}\subset K^{\prime}_{SEAF}\) and \(K^{\prime}_{SEAF}\) is generated for SUPI\({}^{\prime}\). Alternatively, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{l}[\text{UE}^{\prime},\) SN, \(HN,\) SUCI\({}^{\prime},\)\(SNN\), \(RAND\), \(AUTN^{\prime},\)\((HXRES^{*})^{\prime},\)\(MACf\) and an initiator strand \(s\in\text{Init}_{l}[\text{UE}^{\prime},\) SN, \(HN,\) SUCI\({}^{\prime},\)\(RAND\), \(AUTN^{\prime},\)\((RES^{*})^{\prime}]\), where \(SUPI^{\prime}\subset SUCI^{\prime}\), \(SUPI^{\prime}\subset SUCI^{\prime}\), \(K^{\prime}\subset AUTN^{\prime}\) and \(K^{\prime}\subset(HXRES^{*})^{\prime}\). Proof of Theorem 7.: By assumptions (2) and (3), \(K_{SN,HN}\
otin\mathcal{K}_{P}\) and \(RAND\) are uniquely originating in \(\sum\) so \(\{RAND||H_{1}||H_{2}\}_{K_{SN,HN}}=\text{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,\)\(SUCI^{\prime},\)\(SNN\), \(RAND\), \(AUTN^{\prime},\)\((HXRES^{*})^{\prime},\)\((RES^{*})^{\prime},\)\(Result,K^{\prime}_{SEAF},\)\(SUPI^{\prime}]\), where \(SUPI^{\prime}\subset SUCI^{\prime}\), \(K^{\prime}\subset AUTN^{\prime}\), \(K^{\prime}\subset(HXRES^{*})^{\prime}\), \(K^{\prime}\subset(RES^{*})^{\prime}\), \(K^{\prime}\subset K^{\prime}_{SEAF}\) and \(K^{\prime}_{SEAF}\) is generated for \(SUPI^{\prime}\). By assumption (2), \(K^{\prime}\
otin\mathcal{K}_{P}\). Since \(CK^{\prime}=f_{3}(K^{\prime},RAND)\) and \(1  
\(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}_{\uparrow}[UE^{\prime},SN,HN,SUCI^{\prime},RAND,AUTN^{\prime \prime},(RES^{*})^{\prime}]\), where \(SUPI^{\prime}\subset 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}\subset 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}_{\uparrow}[UE^{\prime},SN,HN,SUCI^{\prime\prime},RAND,AUTN^{ \prime},(RES^{*})^{\prime}]\). 2.