# 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
If \(t\) is a server strand of Definition 2, then \(t\in\text{Serv}_{\uparrow}[UE^{\prime},SN,HN,SUCI^{\prime},SNN,RAND,AUTN^{\prime}, (HXRES^{*})^{\prime},\ Syncf,AUTS^{\prime}]\), where \(SUPI^{\prime}\subset SUCI^{\prime}\), \(K^{\prime}\subset AUTN^{\prime}\), \(K^{\prime}\subset(HXRES^{*})^{\prime}\), \(K^{\prime}\subset AUTS^{\prime}\) and \(SQN_{\downarrow IE^{\prime}}\subset AUTS^{\prime}\). By Definition 1, \((RES^{*})^{\prime}=KDF(CK^{\prime}||IK^{\prime},SNN||RAND||RES^{\prime})=term(<r,5>)\). By assumption (2), \(K^{\prime}\
otin\mathcal{K}_{P}\). Since \(CK^{\prime}=f_{3}(K^{\prime},RAND)\) and \(IK^{\prime}=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}=term(<r,5>)\) must originate on an initiator strand \(s\in\text{Init}_{\uparrow}[UE^{\prime},SN,HN,SUCI^{\prime\prime},RAND,AUTN^{ \prime\prime},(RES^{*})^{\prime}]\), where \(SUPI^{\prime}\subset SUCI^{\prime\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}]\). By assumption (2), \(K^{\prime}\
otin\mathcal{K}_{P}\), so \((MAC-S)^{\prime}=f_{1}^{*}(K^{\prime},SQN_{\downarrow IE^{\prime}}||RAND||AMF_{ \circ})\subset AUTS\subset term(<t,3>)\) must originate on an initiator strand \(s^{\prime}\in\text{Init}_{\uparrow}[UE^{\prime},SN^{\prime\prime},HN,SUCI^{ \prime\prime},RAND,AUTN^{\prime\prime},Syncf,AUTS^{\prime}]\), where \(SUPI^{\prime}\subset SUCI^{\prime\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^{\prime},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^{\prime}\in\text{Init}_{\uparrow}[UE^{\prime},SN^{\prime\prime},HN,SUCI^{ \prime\prime},RAND,AUTN^{\prime},(GNF,AUTS^{\prime}]\). By Definition 1, \(SQN_{\downarrow IE^{\prime}}<SQN\) on \(s\). However, \(SQN_{\downarrow IE^{\prime}}\geq SQN\) on \(s^{\prime}\) according to Definition 2. Therefore, \(s\) and \(s^{\prime}\) cannot be in the same run of the protocol, so \(s\) or \(s^{\prime}\) must exist in the past run of the protocol. Since \(s\) or \(s^{\prime}\) exists in the past run of the protocol, \(t\) must exist in the past run of the protocol. Because \((MAC-S)^{\prime}\subset AUTS^{\prime}\subset term(<t,3>)\) originates on \(s^{\prime},s^{\prime}\) must exist in the past run of the protocol, so \(s\) must exist in the current run of the protocol. However, it is impossible from \(SQN_{\downarrow IE^{\prime}}\geq SQN\) to \(SQN_{\downarrow IE^{\prime}}<SQN\) because \(SQN_{\downarrow IE^{\prime}}\) increases. That is to say, it is impossible that \(s^{\prime}\) exists in the past run of the protocol and \(s\) exists in the current run of the protocol. Hence, \(t\) is not a server strand of Definition 2. 3. If \(t\) is a server strand of Definition 3, then \(t\in\text{Serv}_{\uparrow}[UE^{\prime},SN,HN,SUCI^{\prime},SNN,RAND,AUTN^{\prime}, (HXRES^{*})^{\prime},MACf]\), where \(SUPI^{\prime}\subset SUCI^{\prime}\), \(K^{\prime}\subset AUTN^{\prime}\) and \(K^{\prime}\subset(HXRES^{*})^{\prime}\). By Definition 1, \((RES^{*})^{\prime}=KDF(CK^{\prime}||IK^{\prime},SNN||RAND||RES^{\prime})=term(<r,5>)\). By assumption (2), \(K^{\prime}\
otin\mathcal{K}_{P}\).