# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 3 Formal Verification and Analysis of the 5G AKA Protocol
### The Initiator's Guarantee of the 5G AKA Protocol
(1) If \(t\) is a server strand of Definition 1, then \(t\in\mathit{Serv}_{\parallel}\{\mathit{UE},\,\mathit{SN}^{\prime},\,\mathit{HN},\, \mathit{SUCI}^{\prime},\,\mathit{SNN}^{\prime},\,\mathit{RAND},\,\mathit{AUTN},\, \mathit{(HXRES^{*})^{\prime}},\,\mathit{(RES^{*})^{\prime}},\,\mathit{Result},\,K^{ \prime}SEAF,\,\mathit{SUPI}\}\), where \(x^{\prime}\subset\mathit{SUCI}^{\prime}\), \(\mathit{SNN}^{\prime}\subset(HXRES^{*})^{\prime}\), \(\mathit{SNN}^{\prime}\subset(RES^{*})^{\prime}\) and \(\mathit{SNN}^{\prime}\subset K^{\prime}\)'\(\mathit{SEAF}\). By assumption (2), \(K\
otin\mathcal{K}_{p}\). Since \(\mathit{CK}=f_{3}(K,\mathit{RAND})\) and \(\mathit{IK}=f_{4}(K,\mathit{RAND})\), \(\mathit{CK}\
otin\mathcal{K}_{p}\) and \(\mathit{IK}\
otin\mathcal{K}_{p}\), we \(\mathit{CK}||IK\
otin\mathcal{K}_{p}\). Hence, \((RES^{*})^{\prime}=\mathit{KDF}(\mathit{CK}||IK,\mathit{SNN}^{\prime}||RAND|| RES)\)\(\subset term(<t,3>)\) must originate on an initiator strand \(s^{\prime}\in\mathit{Init}_{\parallel}\{\mathit{UE},\,\mathit{SN}^{\prime},\,\mathit{HN}, \mathit{SUCI}^{\prime\prime},\,\mathit{RAND},\,\mathit{AUTN}^{\prime\prime},\, \mathit{(RES^{*})^{\prime}}\}\), where \(\mathit{AUTN}^{\prime\prime}=\mathit{SQN}^{\prime\prime}\oplus\mathit{AK}|| \mathit{MACF}|\mathit{MACF}\) and \(\mathit{MAC}^{\prime\prime}=f_{1}(K,\mathit{SQN}^{\prime\prime}||RAND||AMF)\). Since \(K\
otin\mathcal{K}_{p}\), \(\mathit{MAC}^{\prime\prime}\subset\mathit{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 \(\mathit{SQN}^{w}=\mathit{SQN}\) and \(\mathit{AUTN}^{\prime\prime}=\mathit{AUTN}\). By assumption (1) and Definition 2, \(\mathit{SQN}_{\mathit{UE}}\geq\mathit{SQN}\) on \(s\). However, \(\mathit{SQN}_{\mathit{UE}}<\mathit{SQN}\) on \(s^{\prime}\) according to Definition 1. Therefore, \(s\) and \(s^{\prime}\) cannot be in the same run of the protocol, so \(s^{\prime}\) must exist in the past run of the protocol. Because \(\mathit{SQN}_{\mathit{UE}}\) increases, it is possi  
Figure 5: The fourth attack scenario of the 5G AKA protocol. ble from \(SQN_{UE}<SQN\) to \(SQN_{UE}\geq SQN\). That is to say, it is possible that \(s^{\prime}\) exists in the past run of the protocol and \(s\) exists in the current run of the protocol. Hence, it is possible that \(t\) is a server strand of Definition 1. By assumption (2), \(K_{SN^{\prime},HN}\
ot\in\mathcal{K}_{P}\), so \(\{(RES^{*})^{\prime}\}_{K_{SN^{\prime},HN}}=\mathit{term}(<t,3>)\) must originate on a responder strand \(r\in\mathrm{Resp}_{1}[UE^{\prime\prime},\,SN^{\prime},\,HN,\,SUCI^{\prime \prime},\,SNN^{\prime},\,RAND,\,H^{\prime\prime},\,(HXRES^{*})^{\prime},\,(RES^ {*})^{\prime}\). _Result_, \(K^{\prime\prime}{}_{\mathit{SEAF}},\,SUPI^{\prime\prime}]\), where \(SUPI^{\prime\prime}\subset SUCI^{\prime\prime}\) and \(K^{\prime\prime}{}_{\mathit{SEAF}}\) is generated for \(SUPI^{\prime\prime}\). Since \(K_{SN^{\prime},HN}\
ot\in\mathcal{K}_{P}\), \(\{RAND||H^{\prime\prime}||(HXRES^{*})^{\prime}\}_{K_{SN^{\prime},HN}}=\mathit{ term}(<r,3>)\) must originate on a server strand \(t^{\prime\prime}\). Since \(RAND\) is uniquely originating in \(\sum t^{\prime\prime}=t\), so \(H^{\prime\prime}{}_{1}=AUTN\). Hence, \(r\in\mathrm{Resp}_{1}[UE^{\prime\prime},\,SN^{\prime},\,HN,\,SUCI^{\prime \prime},\,SNN^{\prime},\,RAND,\,AUTN,\,(HXRES^{*})^{\prime},\,(RES^{*})^{\prime}, \,Result,\,K^{\prime\prime}{}_{\mathit{SEAF}},\,SUPI^{\prime\prime}]\). From the above, \(s^{\prime}\) exists in the past run of the protocol and \(MAC\subset AUTN\subset term(<s^{\prime},2>)\) originates on \(t\), so \(t\) must exist in past run of the protocol. From the above, \(\{(RES^{*})^{\prime}\}_{K_{SN^{\prime},HN}}=\mathit{term}(<t,3>)\) originates on \(r\), so \(r\) also must exist in the past run of the protocol. 2.