# A Secure Blockchain-Based Authentication and Key Agreement Scheme for 3 GPP 5G Networks
## 5 Security Evaluation
### Scyther Tool  
The Scyther tool [33] is an automated formal verification tool for analyzing authentication protocols. Under the perfect cryptography assumption and the Dolev-Yao adversary model [30], Scyther searches for all potential security vulnerabilities of a protocol efficiently. Perfect cryptography assumption refers that the cryptographic functions used in the protocol are assumed to be secure. Adversaries should know nothing about the encrypted content unless they hold the decryption key. The Dolev-Yao adversary model, as mentioned in Section 3.2, assumes that there are neighboring attackers in the network. In this section, we model the 5 GSBA with the Security Protocol Description Language (SPDL) and let Scyther find all security issues automatically. The Scyther tool has six different security claims: **Aliveness** or **Alive** ensure the protocol instances complete their steps with any active responders. That is, all replies should be active replies from living partners, not replayed messages. **Niagree** ensures a protocol instance receives the expected variables without consideration of a one-to-one relationship (i.e., non-injective agreement). **Nisynch** ensures the protocol can complete a run as expected without a one-to-one relationship (i.e., non-injective synchronization). **Weakagree** ensures all protocol instances communicate with their same set of initiators or responders (i.e., injective). **Reachable** is the checkpoint claim indicating that the protocol can reach the specific line, which can be used for code debugging. **Secrecy** or **SKR** check if the specified variables or session keys remain secret to adversaries throughout the execution of the protocol. By combining all these security claims, Scyther ensures the injective agreement of the protocol and detects most of the network protocol attacks including message fabrication, message replay, and MITM attacks. Our formal verification result with Scyther is shown in Figure 4. Specifically, we created a SPDL model that has two roles: the gNB and the UE. First, the 5 GSBA can achieve a mutual key agreement using ECDH. To emulate ECDH key exchange between two parties, we define functions g1 and g2, and then set alpha to be g1(a) and beta to be g1(b). We firstly use the claims of Secret a and Secret b to check the secrecy of the ECDH private keys. Then, we emulate the derivation of the ECDH common key with g2(beta, a) (i.e., a \(\cdot\) b \(\cdot\) G) and g2(alpha, b) (i.e., b \(\cdot\) a \(\cdot\) G). We also verify the secrecy of this ECDH common key with _SKR_ claims. Second, the 5 GSBA uses HMAC to ensure the integrity of all messages. To make sure adversaries cannot obtain the HMAC key \(K_{\textit{I}mac}\) (i.e., only gNBs can receive the key from the UE), we check it with Secret Khmac claims for both the gNB and the UE. Third, the 5 GSBA can guarantee device anonymity by encrypting the SUPI into SUCI. To ensure the adversaries have no way to retrieve the SUPI of the UE through the air, we check the secrecy of the SUPI using the Secret MSIN claim. In this scenario, Mobile Subscriber Identification Number (MSIN) is equivalent to SUPI, because SUPI should contain mobile country code (MCC), mobile network code (MNC), and MSIN. While MCC and MNC are not the unique identifiers of a device, we only mandate MSIN to be secret. Fourth, our protocol assumes that the UE needs to use its one-time hash secret Y to prove its identity to gNB. To ensure that the adversaries cannot obtain the secret Y with any means, we checked its secrecy using Secret Y claims. Additionally, the secrecy of Y2 was checked to ensure that the UE could not reveal the next one-time hash secret by any means. Fifth, to further ensure the correctness of our SPDL model, a _Reachable_ claim was put at the end of every role. This made sure that every line of our code had been executed.