# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 4 Our Proposed 5G-AKA' Protocol and Its Security Analysis  
### The 5G-AKA' Protocol  
In order to overcome the above security problems of the latest version of the 5G AKA protocol, we propose a 5G-AKA' protocol, which is illustrated in Figure 23.  
Compared with the latest version of the 5G AKA protocol, the main improvements of our proposed 5G-AKA' protocol are as follows:  
* To cryptographically bind \(x\cdot y\cdot G\) and \(SNN\) to \(K\), and protect \(K\), we replace \(K\) with \(BK\) on the UE and the HN. \[BK=KDF(K,x\cdot y\cdot G||SNN)\] (21) where \(BK\) is a base key derived from \(K\).
* To prevent DoS attacks on the SN, we add the challenge-response mechanism between the SN and the HN. In detail, we add \(RAND_{5N}\) to the first three messages between the SEAF (located in the SN) and the AUSF (located in the HN) and add \(RAND\) to the fourth message between the SEAF and the AUSF, where \(RAND_{5N}\) is an unpredictable challenge of the SEAF;  
Figure 21: The twentieth attack scenario of the 5G AKA protocol.  
Figure 22: The twenty-first attack scenario of the 5G AKA protocol.  
* Add \(SUPI\) to the second message between the SEAF and the AUSF, matching with \(SUCI\) in the first message between them;
* In the latest version of the 5G AKA protocol, \(MACf\) is used to initiate a new authentication procedure for the UE. However, it causes a large number of attacks according to the above security analysis. Hence, we use a timeout mechanism on the HN instead of \(MACf\) to initiate a new authentication procedure towards the UE. That is to say, if \(XMAC\) and \(MAC\) are different, then the UE directly discards the receives \(RAND||AUTN\), and the HN will initiate a new authentication procedure towards the UE when the HN does not receive an authentication response message or a synchronization failure message within a certain period of time.  
According to the above descriptions, our proposed 5G-AKA' protocol can be summarized into two cases as follows:  
Case (I): the verification of \(AUTN\) succeeds and the authentication is successful. The steps of this case are as follows:  
1. \(UE\to SN\): \(SUCI\);
2. \(SN\to HN\): \(\{RAND_{SN}||SUCI||SNN\}_{K_{SN,HN}}\);
3. \(HN\to SN\): \(\{RAND_{SN}||SUPI||RAND||AUTN||HXRES^{*}\}_{K_{SN,HN}}\);
4. \(SN\to UE\): \(RAND||AUTN\);
5. \(UE\to SN\): \(RES^{*}\);
6. \(SN\to HN\): \(\{RAND_{SN}||RES^{*}\}_{K_{SN,HN}}\);
7. \(HN\to SN\): \(\{RAND||Result||K_{SEAF}||SUPI\}_{K_{SN,HN}}\).  
where \(SUCI\), \(RAND||AUTN\) and \(RES^{*}\) are three messages exchanged between the UE and SN, \(\{RAND_{SN}||SUCI||SNN\}_{K_{SN,HN}}\), \(\{RAND_{SN}||SUPI||RAND||AUTN||HXRES^{*}\}_{K_{SN,HN}}\), \(\{RAND_{SN}||RES^{*}\}_{K_{SN,HN}}\) and \(\{RAND||Result||K_{SEAF}||SUPI\}_{K_{SN,HN}}\) are four messages exchanged between the SN and the HN.  
Case (II): the verification of \(AUTN\) fails and it is a synchronization failure. The steps of this case are as follows:  
1. \(UE\to SN\): \(SUCI\);
2. \(SN\to HN\): \(\{RAND_{SN}||SUCI||SNN\}_{K_{SN,HN}}\);
3. \(HN\to SN\): \(\{RAND_{SN}||SUPI||RAND||AUTN||HXRES^{*}\}_{K_{SN,HN}}\);
4. \(SN\to UE\): \(RAND||AUTN\);  
Figure 23: Our proposed 5G-AKA’ protocol.  
\(UE\to SN\): \(S\)\(\mathit{syncf}||AUTS\);
6. \(SN\to HN\): \(\{RAND_{SN}||S\mathit{yncf}||RAND||AUTS\}_{K_{SN,HN}}\).  
where \(S\)\(\mathit{SUCI}\), \(RAND||AUTN\) and \(\mathit{Syncf}||AUTS\) are three messages exchanged between the UE and SN, \(\{RAND_{SN}||S\mathit{UCI}||SNN\}_{K_{SN,HN}}\), \(\{RAND_{SN}||S\mathit{UPI}||RAND\\ ||AUTN||HXRES^{*}\}_{K_{SN,HN}}\) and \(\{RAND_{SN}||S\mathit{yncf}||RAND||AUTS\}_{K_{SN,HN}}\) are three messages exchanged between the SN and the HN.  
In the above cases, \(K\) is replaced with \(BK\). Similarly, we use the mixed strand space model [28] to analyze the security of our proposed 5G-AKA' protocol as follows.