# A Secure and Efficient Authentication Scheme for Fog-Based Vehicular Ad Hoc Networks
## 5 Security Analysis
### Formal Analysis
#### 5.1.6 Burrows-Abadi-Nikoogadam (BAN) Logic Proof  
The BAN logic proof is based on the following assumptions and idealized forms:  
**S 1:**: \(FN_{j}\) receives \(D_{1}\).  
\[S_{1}\text{: }FN_{j}\lhd(R_{1},Q_{i})_{N_{i}}\]
**S 2:**: \(CS\) receives \(D_{2}\).  
\[S_{2}\text{: }CS\lhd(R_{1},R_{2},r_{2}R_{1},L_{j})_{N_{j}}\]
**S 3:**: Applying \(S_{2}\) and \(A_{11}\) to the MMR yields \(S_{3}\).  
\[S_{3}\text{: }CS|\equiv FN_{j}|\sim(R_{1},R_{2},r_{2}R_{1},L_{j})\]
**S 4:**: Applying \(S_{3}\) and \(A_{4}\) to the FR yields \(S_{8}\).  
\[S_{4}\text{: }CS|\equiv\#(R_{1},R_{2},r_{2}R_{1},L_{j})\]
**S 5:**: Applying \(S_{3}\) and \(S_{4}\) to the NVR yields \(S_{5}\).  
\[S_{5}\text{: }CS|\equiv FN_{j}|\equiv(R_{1},R_{2},r_{2}R_{1},L_{j})\]
**S 6:**: We can obtain \(S_{6}\) by applying \(S_{5}\) to the BR.  
\[S_{6}\text{: }CS|\equiv FN_{j}|\equiv(r_{2}R_{1})\]
**S 7:**: \(FN_{j}\) receives \(D_{3}\).  
\[S_{7}:FN_{j}\trianglelefteq(R_{3},r_{3}R_{1},h(N_{i}\parallel R_{i-j-cs}))h(N_{j }\parallel R_{i-j-\alpha})\]  
**S 8:**: Applying \(S_{7}\) and \(A_{10}\) to the MMR yields \(S_{8}\).  
\[S_{8}:FN_{j}\equiv CS\mid\sim(R_{3},r_{3}R_{1},h(N_{i}\parallel R_{i-j-cs}))\]
**S 9:**: Applying \(S_{8}\) and \(A_{3}\) to the FR yields \(S_{9}\).  
\[S_{9}:FN_{j}\equiv\#(R_{3},r_{3}R_{1},h(N_{i}\parallel R_{i-j-cs}))\]
**S 10:**: Applying \(S_{8}\) and \(S_{9}\) to the NVR yields \(S_{10}\).  
\[S_{10}:FN_{j}\equiv CS\mid\equiv(R_{3},r_{3}R_{1},h(N_{i}\parallel R_{i-j-cs}))\]
**S 11:**: We can obtain \(S_{11}\) by applying \(S_{10}\) to the BR.  
\[S_{11}:FN_{j}\mid\equiv CS\mid\equiv(r_{3}R_{1})\]
**S 12:**: \(V_{i}\) receives \(D_{4}\).  
\[S_{12}:V_{i}\trianglelefteq(r_{2}R_{3},h(N_{j}\parallel R_{i-j-cs}))_{h(N_{ i}\parallel R_{i-j-\alpha})}\]
**S 13:**: Applying \(S_{12}\) and \(A_{9}\) to the MMR yields \(S_{13}\).  
\[S_{13}:V_{i}\equiv FN_{j}\mid\sim(r_{2}R_{3},h(N_{j}\parallel R_{i-j-cs}))\]
**S 14:**: Applying \(S_{13}\) and \(A_{1}\) to the FR yields \(S_{14}\).  
\[S_{14}:V_{i}\mid\equiv\#(r_{2}R_{3},h(N_{j}\parallel R_{i-j-cs}))\]
**S 15:**: Applying \(S_{13}\) and \(S_{14}\) to the NVR yields \(S_{15}\).  
\[S_{15}:V_{i}\mid\equiv FN_{j}\mid\equiv(r_{2}R_{3},h(N_{j}\parallel R_{i-j-cs}))\]
**S 16:**: We can obtain \(S_{16}\) by applying \(S_{15}\) to the BR.  
\[S_{16}:V_{i}\equiv FN_{j}\mid\equiv(r_{2}R_{3})\]
**S 17:**: From \(S_{6}\), \(S_{11}\), and \(S_{16}\), \(V_{i}\), \(FN_{j}\), and \(CS\) can compute the session key \(SK_{i-j-cs}=h(h(N_{i}\parallel R_{i-j-cs})\parallel h(N_{j}\parallel R_{i-j-cs})\parallel R _{i-j-cs})\).  
\[S_{17}:V_{i}\equiv FN_{j}\mid\equiv V_{i}\stackrel{{ SF}}{{ \longleftrightarrow}} FN_{j}\] **(Goal 2)** \[S_{18}:FN_{j}\mid\equiv V_{i}\equiv V_{i}\stackrel{{ SF}}{{ \longleftrightarrow}} FN_{j}\] **(Goal 4)** \[S_{19}:FN_{j}\mid\equiv CS\mid\equiv CS\stackrel{{ SF}}{{ \longleftrightarrow}} FN_{j}\] **(Goal 6)** \[S_{20}:CS\mid\equiv FN_{j}\mid\equiv CS\stackrel{{ SF}}{{ \longleftrightarrow}} FN_{j}\] **(Goal 8)**  
**S 18:**: The JR can be applied to \(S_{21},S_{22},S_{23}\), and \(S_{24}\) using \(A_{5}\), \(A_{8}\), \(A_{6}\), and \(A_{7}\), respectively.  
\[S_{21}:V_{i}\mid\equiv V_{i}\stackrel{{ SF}}{{ \longleftrightarrow}} FN_{j}\] **(Goal 1)** \[S_{22}:FN_{j}\mid\equiv V_{i}\stackrel{{ SF}}{{ \longleftrightarrow}} FN_{j}\] **(Goal 3)** \[S_{23}:FN_{j}\mid\equiv CS\stackrel{{ SF}}{{ \longleftrightarrow}} FN_{j}\] **(Goal 5)** \[S_{24}:CS\mid\equiv CS\stackrel{{ SF}}{{ \longleftrightarrow}} FN_{j}\] **(Goal 7)**  
Finally, the vehicle user, fog node, and cloud server mutually authenticate each other.