# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 5 Discussion
### Performance of the 5G-AKA' Protocol  
The comparative analysis between the 5G-AKA' protocol and some recently improved 5G AKA protocols [22; 23; 24] in the number of messages, the number of fields, the amount of calculation and backward compatibility is shown in Table 3.  
In Table 3, \(MN\) denotes the number of messages of the 5G AKA protocol. \(FN\) denotes the number of fields of the 5G AKA protocol. \(CA\) denotes the amount of calculation of the 5G AKA protocol. Note that the number of messages and the number of fields in Table 3 are the number of messages and the number of fields among the UE, the SN and the HN. \(ECDH\) denotes the generation and verification of an elliptic curve Diffie-Hellman (ECDH) exchange. \(PED\) denotes the encryption and decryption based on a public and private key pair. \(F\) denotes the generation and verification of a key function, a key derivation function, a MAC function or a hash function, which are grouped into one category because they have a similar amount of calculation [27]. According to [26], the computation overhead of the generation or verification of an ECDH exchange is 1290 us, the computation overhead of the encryption based on a public key is 2580 us, the computation overhead of the decryption based on a private key is 1750 us, the computation overhead of the hash function based on SHA-256 is 3.8 us, and the computation overhead of the MAC function based on HMAC-SHA256 is 67 us.  
\begin{table}
\begin{tabular}{c c c c c c} \hline \hline
**Comparative Items** & **5G AKA** & [22] & [23] & [24] & **5G-AKA’** \\ \hline The number of messages & \(MN\) & \(MN\) & \(MN\) & \(MN\) & \(MN\)-2 \\ The number of fields & \(FN\) & \(FN\) + 9 & \(FN\)-1 & \(FN\) + 2 & \(FN\) + 4 \\ The amount of calculation & \(CA\) & \(CA\) + 2\(F\) & \(CA\) + 4\(PED\)-1\(ECDH\)-2\(F\) & \(CA\) + 2\(PED\) + 1\(F\) & \(CA\) + 1\(F\) \\ Backward compatibility & – & Yes & No & No & Yes \\ \hline \hline \end{tabular}
\end{table}
Table 3: The comparative analysis between the 5G-AKA’ protocol and some recently improved 5G AKA protocols [22; 23; 24] in the number of messages, the number of fields, the amount of calculation and backward compatibility.  
In our proposed 5G-AKA' protocol, two messages related to \(MACf\) are cut down because \(MACf\) is replaced with a timeout mechanism on the HN. Four \(RAND_{SN}\), one \(RAND\), and one \(SUPI\) are added to the messages between the SN and the HN, while two \(MACf\) are cut down, so four fields are added. Since \(K\) is replaced with \(BK=KDF(K,x\cdot y\cdot G||SNN)\) on the UE and the HN, the calculation amount of one \(F\) is added. From Table 3, compared with other protocols, our proposed 5G-AKA' protocol reduces two messages. The 5G-AKA' protocol adds more fields than the protocols in [23] and [24], but less than the protocol in [22]. In the amount of calculation, our proposed 5G-AKA' protocol increases the least, while the protocols in [23] and [24] increase the most because they introduce multiple public-key encryption and decryption. Hence, our proposed 5G-AKA' protocol is efficient. Especially for the UE, only a key derivation function is added, but one field and one message are reduced.  
In addition, the protocols in [23] and [24] destroys the structure of the messages instead of adding fields to the messages or extending fields in the messages, so they are not backward compatible. Our proposed 5G-AKA' protocol only extends \(K\) and adds some fields to the messages between the SN and the HN, so it is forward compatible.