# An Enhanced Privacy-Preserving Authentication Scheme for Vehicle Sensor Networks
## 6 Analysis
### Correctness
#### Idealization  
First, we use formal logical language to idealize the general authentication procedure in our improved scheme in accordance with the rules of the BAN logic as follows:  
(1). \(OBU_{i}\to LE_{j}\) : \(\{M_{1}=h(r_{i}\|AID_{i}\|C_{i}\|y_{i}),AID_{i},\{r_{i}\}_{A_{i^{\prime}}}\{A_ {i}\}_{PSK}\}\),  
(2). \(LE_{j}\to OBU_{i}\) : \(\{M_{2}=h(AID_{j}\|SK_{ij}\|r_{j}\|PSK),AID_{j},\{r_{j}\}_{r_{i}},\{PSK\}_{r_{ j}}\}\),  
(3). \(OBU_{i}\to LE_{j}\) : \(\{M_{3}=SK_{ij}\oplus h(r_{j})\). Goal  
There are two roles in the general authentication procedure: \(OBU_{i}\) and \(LE_{j}\). Since \(OBU_{i}\) needs to obtain the authorized parameter \(PSK\) from the \(LE_{j}\), it must believe \(PSK\). Moreover, \(OBU_{i}\) and \(LE_{j}\) must believe each other and each other's aliases, and they must believe the session key computed in the general authentication procedure. Thus, there are five goals of the general authentication procedure in our improved scheme as follows:  
1. \(OBU_{i}\mid\equiv LE_{j}\mid\equiv PSK\): \(OBU_{i}\) believes \(PSK\). 2. \(OBU_{i}\mid\equiv LE_{j}\mid\equiv AID_{j}\): \(OBU_{i}\) believes \(LE_{j}\) and his alias \(AID_{j}\). 3. \(LE_{j}\mid\equiv OBU_{i}\mid\equiv AID_{i}\): \(LE_{j}\) believes \(OBU_{i}\) and his alias \(AID_{i}\). 4. \(OBU_{i}\mid\equiv OBU_{i}\stackrel{{ SK_{ij}}}{{\longleftrightarrow}}LE_{j}\): \(OBU_{i}\) believes the share key between himself and \(LE_{j}\). 5. \(LE_{j}\mid\equiv LE_{j}\stackrel{{ SK_{ij}}}{{\longleftrightarrow}}OBU_{i}\): \(LE_{j}\) believes the share key between himself and \(OBU_{i}\). Assumptions  
With the goals set, the assumptions also need to be stated as follows: \begin{table}
\begin{tabular}{l c} \hline \hline
**Symbol** & **Description** \\ \hline \(P\mid\equiv X\) & Entity \(P\) trusts opinion \(X\) \\ \(P\triangleleft X\) & Entity \(P\) sees opinion \(X\), or \(P\) holds \(X\) \\ \(P\mid\sim X\) & Entity \(P\) has said opinion \(X\) \\ \(P\mid\Rightarrow X\) & Entity \(P\) completely control over \(X\) \\ \(\sharp(X)\) & \(X\) is fresh \\ \(Rule1\) & \(Rule2\) comes from \(Rule1\) \\ \(\stackrel{{ k}}{{\longleftrightarrow}}P\) & \(k\) is the public key of entity \(P\) \\ \(P\stackrel{{ k}}{{\longleftrightarrow}}Q\) & \(k\) is a secret key or information between \(P\) and \(Q\) \\ \(\{X\}_{PSK}\) & \(X\) is encrypted by key \(K\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Symbol and description of BAN logic. 1. \(OBU_{i}\triangle AID_{i}\): \(OBU_{i}\) possesses an alias \(AID_{i}\). 2. \(LE_{j}\triangleleft AID_{j}\): \(OBU_{j}\) possesses an alias \(AID_{j}\). 3. \(OBU_{i}\mid\equiv\sharp(r_{i}r_{j})\): \(OBU_{i}\) believes the freshness of \(r_{i}\) and \(r_{j}\). 4. \(LE_{j}\mid\equiv\sharp(r_{i}r_{j},y_{i})\): \(LE_{j}\) believes the freshness of \(r_{i}\), \(r_{j}\) and \(y_{i}\). 5. \(LE_{j}\mid\equiv LE_{j}\overset{PSK}{\longleftrightarrow}OBU_{i}\): \(LE_{j}\) believes the share key \(PSK\) between himself and \(OBU_{i}\). 6. \(OBU_{i}\mid\equiv OBU_{i}\overset{r_{i}}{\longleftrightarrow}LE_{j}\): \(OBU_{i}\) believes the share key \(r_{i}\) between himself and \(LE_{j}\). 7. \(LE_{j}\mid\equiv LE_{j}\overset{r_{j}}{\longleftrightarrow}OBU_{i}\): \(LE_{j}\) believes the share key \(r_{j}\) between himself and \(OBU_{i}\). Verification  
In this subsection, we will verify the correctness of our proposed general authentication procedure using the BAN logic. The detailed steps of the proof are as follows:  
\(OBU_{i}\) computes \(AID_{i}\) and \(\{r_{i}\}_{A_{i}}\) :  
1. \(\frac{LE_{j}\triangleleft\{r_{i}\}_{A_{i}}AID_{i}\{A_{i}\}_{PSK},M_{2},y_{i} LE_{j}\mid=LE_{j}\overset{PSK}{\longleftrightarrow}OBU_{i}\)}{OBU_{i}\square OBU_{i} \sim M_{2}}\),
2. \(\frac{LE_{j}\mid=\equiv\sharp(r_{i},y_{i}),LE_{j}\mid=OBU_{i}\sim M_{2}}{LE_{j} \mid=OBU_{i}\mid=M_{2}}\),
3. \(\frac{LE_{j}\mid=OBU_{i}\mid=M_{2}}{LE_{j}\mid=OBU_{i}\mid=AID_{i}}\),  
\(LE_{j}\) computes \(LE_{j}\overset{SK_{ij}}{\longleftrightarrow}OBU_{i}\), \(\{r_{j}\}_{r_{i}}\), \(\{PSK\}_{r_{j}}\),
4.