# 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
By assumptions (2) and (3), \(K_{\mathit{SN},\mathit{HN}}\
otin\mathcal{K}_{P}\) and \(\mathit{RAND}^{\prime}{}_{\mathit{SN}}\) are uniquely originating in \(\sum\) so \(\{RAND^{\prime}{}_{\mathit{SN}}||\mathit{Syncf}||\mathit{RAND}||\mathit{ AUITS}\}_{K_{\mathit{SN},\mathit{HN}}}=term(<t,3>)\) must originate on a unique respondar strand \(r\in\mathrm{Resp}_{\mathrm{II}}[\mathit{UE}^{\prime},\mathit{SN},\mathit{HN}, \mathit{SUPI}^{\prime},\mathit{SUCI}^{\prime}]\), \(\mathit{SNN},\mathit{RAND}^{\prime}{}_{\mathit{SN}},\mathit{RAND},\mathit{ H}^{\prime}{}_{\mathit{1}},\mathit{H}^{\prime}{}_{\mathit{2}},\mathit{Syncf},\mathit{AUTN}]\), where \(\mathit{SUPI}^{\prime}\subset\mathit{SUCI}^{\prime}\). Since \(K_{\mathit{SN},\mathit{HN}}\
otin\mathcal{K}_{P}\), \(\{RAND^{\prime}{}_{\mathit{SN}}||\mathit{SUPI}^{\prime}||\mathit{RAND}|| \mathit{H}^{\prime}{}_{\mathit{1}}||\mathit{H}^{\prime}{}_{\mathit{2}}\}_{K_{ \mathit{SN},\mathit{HN}}}=term(<r,3>)\) must originate on a server strand \(t^{\prime}\). Since \(RAND\) is uniquely originating in \(\sum\)\(t^{\prime}=t\), so \(\mathit{SUPI}^{\prime}=\mathit{SUPI}\), \(\mathit{UE}^{\prime}=\mathit{UE}\), \(\mathit{H}^{\prime}{}_{\mathit{1}}=\mathit{AUTN}\) and \(\mathit{H}^{\prime}{}_{\mathit{2}}=\mathit{HXRES}^{*}\). Since \(K_{\mathit{SN},\mathit{HN}}\
otin\mathcal{K}_{P}\), \(\{RAND^{\prime}{}_{\mathit{SN}}||\mathit{SUCI}||\mathit{SNN}\}_{K_{\mathit{SN}, \mathit{HN}}}=term(<t,1>)\) must originate on a respondar strand \(r^{\prime}\). Since \(\mathit{RAND}^{\prime}{}_{\mathit{SN}}\) is uniquely originating in \(\sum r^{\prime}=r\), so \(\mathit{SUCI}^{\prime}{}^{\prime}=\mathit{SUCI}\). Hence, \(r\in\mathrm{Resp}_{\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{AUTS}]\). \(\Box\)  
According to Theorems 10 and 11, \(\mathit{UE}\) successfully authenticates \(HN\) and \(SN\), and all fields except \(\mathit{RAND}^{\prime}{}_{\mathit{SN}}\) on the sever strand and the responder are agreed with the UE. \(\mathit{RAND}^{\prime}{}_{\mathit{SN}}\) is unknowable to the UE because it is mainly used for the challenge-response mechanism between the SN and the HN, which does not affect the security of the 5G-AKA' protocol. Hence, MitM attacks are prevented. In addition, those attacks in Section 3.2 are overcome as follows:  
1. Since \(BK=\mathit{KDF}(K,x\cdot y\cdot G||\mathit{SNN})\) is used to calculate \(\mathit{AUTN}\), the challenge of the UE (i.e., \(x\)), the pre-shared key between the UE and the HN (i.e., \(K\)) and \(\mathit{SNN}\) are included in \(\mathit{AUTN}\). As a result, \(\mathit{UE}\) can find whether \(\mathit{SUCI}\) is replayed, \(\mathit{UE}\) successfully authenticates \(HN\) and \(\mathit{SN}\), and \(\mathit{RAND}||\mathit{AUTN}\) on the UE cannot be replayed, making that the location privacy of the UE cannot be compromised. 2. Since \(\mathit{MACf}\) is replaced with a timeout mechanism on the HN, MAC failure attacks are prevented. Further, \(\mathit{RAND}||\mathit{AUTN}\) on the UE cannot be replayed maliciously to generate \(\mathit{Syncf}\). As a result, the penetrator cannot take advantage of \(\mathit{Syncf}\) and \(\mathit{MACf}\) to performed cross attacks.