# A Secure Blockchain-Based Authentication and Key Agreement Scheme for 3 GPP 5G Networks
## 5 Security Evaluation
### Burrows-Abadi-Needham (BAN) Logic
#### 5.1.4 Protocol Verification  
The detailed verification steps are listed below. Using the rule with Message 1, we have Equation (19):  
\[\frac{C\mid\equiv U\stackrel{{ Y}}{{\leftrightarrow}}C,\ C\lhd \left\{\langle U\stackrel{{ K_{\textit{Iplace}}}}{{ \leftrightarrow}}C,\ Y\rangle_{Y}\right\}_{\textit{P}K_{\textit{core}}}}{C \lhd\langle U\stackrel{{ K_{\textit{Iplace}}}}{{ \leftrightarrow}}C,\ Y\rangle_{Y}} \tag{19}\]  
Using the message meaning rule with Equations (13) and (19), we have Equation (20):  
\[\frac{C\mid\equiv U\stackrel{{ Y}}{{\leftrightarrow}}C,\ C\lhd \langle U\stackrel{{ K_{\textit{Iplace}}}}{{\leftrightarrow}}C,\ Y \rangle_{Y}}{C\mid\equiv U\mid\sim\ \left(U\stackrel{{ K_{\textit{Iplace}}}}{{ \leftrightarrow}}C,\ Y\right)} \tag{20}\]  
Using the freshness rule with Equations (14) and (19), we have Equation (21):  
\[\frac{C\mid\equiv\#(Y)}{C\mid\equiv\#(U\stackrel{{ K_{\textit{Iplace}} }}{{\leftrightarrow}}C,\ Y)} \tag{21}\]  
Using the nonce verification rule with Equations (20) and (21), we have Equation (22):  
\[\frac{C\mid\equiv U\mid\equiv\left(U\stackrel{{ K_{\textit{Iplace}} }}{{\leftrightarrow}}C,\ Y\right),\ C\mid\equiv U\mid\sim\ \#(K_{\textit{Iplace}},\ Y)}{C\mid\equiv U\mid\equiv\left(U \stackrel{{ K_{\textit{Iplace}}}}{{\leftrightarrow}}C,\ Y\right)} \tag{22}\]  
Using the belief rule with Equation (22), we have Equation (23):  
\[\frac{C\mid\equiv U\mid\equiv\left(U\stackrel{{ K_{\textit{Iplace}} }}{{\leftrightarrow}}C,\ Y\right)}{C\mid\equiv U\mid\equiv U\stackrel{{ K_{\textit{Iplace}}}}{{ \leftrightarrow}}C}=C\mid\equiv U\mid\equiv U\stackrel{{ K_{\textit{Iplace}}}}{{ \leftrightarrow}}C \tag{23}\]  
Using the jurisdiction rule with Equations (1) and (23), we have Equation (24):  
\[\frac{C\mid\equiv U\mid\Rightarrow U\stackrel{{ K_{\textit{Iplace}} }}{{\leftrightarrow}}C,\ C\mid\equiv U\stackrel{{ K_{\textit{Iplace}}}}{{ \leftrightarrow}}C}{C\mid\equiv U\stackrel{{ K_{\textit{Iplace}}}}{{ \leftrightarrow}}C}=C\mid\equiv U\stackrel{{ K_{\textit{Iplace}}}}{{ \leftrightarrow}}C \tag{24}\]As a result, the CN believes the received HMAC key, so the CN continues to process Message 1. Using the message meaning rule with Equation (24) and Message 1, we have Equation (25):  
\[\frac{C\mid\equiv\,U\,^{K_{\text{base}}}C,\,C\,\subset\,\{\,TS,\,a\!\cdot\!P\,\} _{K_{\text{base}}}}{C\mid\equiv\,U\mid\,\sim\,(TS,\,a\!\cdot\!P)}\,=C\mid\equiv \,U\mid\,\sim\,(TS,\,a\!\cdot\!P) \tag{25}\]  
Using the freshness rule with Equations (2) and (25), we have Equation (26):  
\[\frac{C\mid\equiv\,\#(TS)}{C\mid\equiv\,\#(TS,\,a\!\cdot\!P)}=C\mid\equiv\,\#( TS,\,a\!\cdot\!P) \tag{26}\]  
Using the nonce verification rule with Equations (25) and (26), we have Equation (27):  
\[\frac{C\mid\equiv\,\#(TS,\,a\!\cdot\!P)\,\,,\,\,\,C\mid\equiv\,U\mid\sim\,(TS, \,a\!\cdot\!P)}{C\mid\equiv\,U\mid\equiv\,(TS,\,a\!\cdot\!P)} \tag{27}\]  
Using the belief rule with Equation (27), we have Equation (28):  
\[\frac{C\mid\equiv\,U\mid\equiv\,(TS,\,a\!\cdot\!P)}{C\mid\equiv\,U\mid\equiv\, a\!\cdot\!P}=C\mid\equiv\,U\mid\equiv\,a\!\cdot\!P \tag{28}\]  
Using the jurisdiction rule with Equations (10) and (28), we have Equation (29):  
\[\frac{C\mid\equiv U\stackrel{{ Y}}{{\leftrightarrow}}C,\ C\lhd \langle U\stackrel{{ K_{\textit{Iplace}}}}{{\leftrightarrow}}C,\ Y \rangle_{Y}}{C\mid\equiv U\mid\sim\ \left(U\stackrel{{ K_{\textit{Iplace}}}}{{ \leftrightarrow}}C,\ Y\right)} \tag{20}\]0  
As a result, the CN believes the received ECDH public key from UE, and the protocol continues with Message 2.