# Virtual Pseudonym-Changing and Dynamic Grouping Policy for Privacy Preservation in VANETs
## 5 Formal Modeling and Specification
### Formal Modeling and Analysis of Position-Mixing Method  
In this section, we formally model the adversary scenario of the position-mixing method. We design the HLPN of position-mixing algorithm with an attacker scenario shown in Figure 13. The symbols and places used in the HLPN are shown in Tables 6 and 7, respectively. The HLPN for the position-mixing method takes input transition that consists of data about the vehicle neighborhood, neighbor threshold, and neighboring vehicles' position coordinates. First, the vehicle will search for a neighbor in the vicinity and select the concerned neighbor as a position mixer. \begin{table}
\begin{tabular}{l l} \hline \hline
**Symbol** & **Description** \\ \hline CallDist & Distance calculation with neighbor vehicles \\ IDMatching & Linking of vehicle identities used for various timestamp \\ LM & Location mixer \\ LOCMsg & Vehicle location messages \\ LOCMatching & Matching visited locations of a vehicle \\ LS & Location Server \\ MaxDist & Maximum distance range with a \(T_{x}\) neighbor \\ NeighSelection & Selection of neighbor vehicle as a position mixer \\ NF & Neighbor Function \\ OutRange & The vehicle that gets out of the transmission range \\ RandSelect & Random selection of neighbor vehicle \\ SameDist & \(T_{x}\) vehicle are in the same distance range \\ SelectMax & Select a neighbor with a maximum distance range \\ SendQ & Sending of query to LS for location finding \\ TakePOS & Taking of position coordinates \\ VLD & Vehicle location data \\ VIdentity & Vehicle identity \\ \hline \hline \end{tabular}
\end{table} 
Table 6: Symbols used in HLPN for position-mixing method. The neighbor function is used to find transmission range neighbors in the vicinity of a vehicle. Equation (42) shows the success of finding neighboring vehicles and ready to calculate distance among neighboring vehicles. However, the search may be unsuccessful due to the vehicle falling out of range of a group as specified in Equation (43). In Equation (44), the target vehicle will try again to search for vehicles in the transmission range. \[ \begin{split}\textbf{R(FindSuccess)}=\forall\ i2\in x2\wedge i3\in x3 \mid(i3[1]\wedge i3[2]\in i2[2])\\ \wedge x3^{\prime}:=x3\cup\{i3[3]\}.\end{split}  \tag{42}\]  
\[ \begin{split}\textbf{R(FindFail)}=\exists\ i4\in x4\wedge i5\in x 5\mid(i4[2]\
eq i5[2]\wedge i4[3]\
eq i5[3])\\ \wedge OutofRange(x5^{\prime}:=x5\cup\{i5[4]\}).\end{split}  \tag{43}\]  
\[ \begin{split}\textbf{R(SearchAgain)}=\forall\ i6\in x6\wedge i7 \in x7\mid(i6[2]\
eq i7[2])\rightarrow\\ search(x7^{\prime}:=x7\cup\{i7[2],i7[3]\}.\end{split}  \tag{44}\] \begin{table}
\begin{tabular}{l l} \hline \hline
**Symbol** & **Description** \\ \hline \(\varphi\) (NF) & \(P(G_{ID}\times T_{x}\times VL_{R}\times D)\) \\ \(\varphi\) (CalDist) & \(P(G_{ID}\times T_{x}\times Dist(V_{i},V_{j}))\) \\ \(\varphi\) (OutRange) & \(P(G_{ID}\times T_{x}\times VL_{R}\times NotinRange)\) \\ \(\varphi\) (NeighSelection) & \(P(G_{ID}\times T_{x}\times VL_{R}\times SameDist\times MaxDist)\) \\ \(\varphi\) (GH) & \(P(G_{ID}\times P_{ID}\times Verify)\) \\ \(\varphi\) (LM) & \(P(G_{ID}\times P_{ID}\times Tx\times MaxDist\times Mixer_{j})\) \\ \(\varphi\) (Positions) & \(P(G_{ID}\times P_{ID}\times T_{x}\times SameDist\times RandMixer)\) \\ \(\varphi\) (MsgExchange) & \(P(G_{ID}\times T_{x}\times POS_{i}\times POS_{j})\) \\ \(\varphi\) (LS) & \(P(G_{ID}\times VL\times MixLOC\times ReqLOC)\) \\ \(\varphi\) (Vehicle) & \(P(G_{ID}\times P_{ID}\times InterestLOC)\) \\ \(\varphi\) (LOCMsg) & \(P(G_{ID}\times P_{ID}\times VL\times D\times LOC_{i})\) \\ \(\varphi\) (OldPseudo) & \(P(G_{ID}\times OldP_{ID}\times LOC\times TS)\) \\ \(\varphi\) (VIentify) & \(P(G_{ID}\times P_{ID}\times VL\times D\times LOC_{i}\times Expose)\) \\ \hline \hline \end{tabular}
\end{table} 
Table 7: Places used in HLPN for position-mixing method. Figure 13: HLPN of position-mixing algorithm. After finding neighbors in the transmission range, the distance between them is calculated as given in Equation (45).