# 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
The target vehicle will compare the distance to its neighbors. The neighboring vehicle with maximum distance is selected as a position mixer shown in Equation (46). If the neighbors are in the same distance ranges, then the target vehicle will randomly choose one of the vehicles in its neighbor list specified in Equation (47). In both equations Equations (46) and (47), the selected neighboring vehicle identity is verified with GH's help. \[ \begin{split}\textbf{R(Distance)}=\forall\ i8\in x8\wedge i9\in x9 \mid(i9[2]\wedge i9[3]\in i8[2])\wedge\\ Calculate(x9^{\prime}:=x9\cup\{i9[4],i9[5]\}.\end{split}  \tag{45}\]  
\[ \begin{split}\textbf{R(SelectMax)}=\forall\ i10\in x10\wedge i1 1\in x11\wedge i12\in x12\mid(i12[1]=i10[1]\wedge i12[3]=\\ i10[2])\wedge(i12[2]=i11[2])\to Verify\wedge x12^{\prime}:=x12\cup\{i12[ 4],i12[5]\}.\end{split}  \tag{46}\]  
\[ \begin{split}\textbf{R(RandSelect)}=\forall\ i13\in x13\wedge i14 \in x14\wedge i15\in x15\mid(i15[1]=i13[1]\wedge\\ i15[5]=i13[5])\wedge(i15[2]=i14[2])\to Verify\wedge x15^{\prime}:=x15 \cup\{i15[5]\}.\end{split}  \tag{47}\]  
Once the target vehicle selects its position mixer, the position-mixing procedure is invoked. Each vehicle will take its position coordinates and exchange it with its neighboring vehicle chosen, as shown in Equation (48). The position-mixing query is prepared by each vehicle and sent to the location server as specified in Equation (49). On calculating the location query, the location server responds to the vehicle with the desired location, such as the nearest restaurant, gas station, and hospital locations; see Equation (50). \[ \begin{split}\textbf{R(TakePOS)}=\forall\ i16\in x16\wedge i17\in x 17\wedge i18\in x18\mid(i16[1]\wedge i17[1])\\ \in i18[1]\wedge(i16[3]\wedge i17[3])\in i18[2]\wedge Select(i16[5] ori17[5])\\ \to Exchange(x18^{\prime}:=x18\cup\{i18[3],i18[4]\}).\end{split}  \tag{48}\]  
\[ \begin{split}\textbf{R(SendQ)}=\forall\ i19\in x19\wedge i20\in x 20\mid(i19[1]=i20[2])\wedge\\ QueryRequest(x20^{\prime}:=x20\cup\{i20[3],i20[4]\}).\end{split}  \tag{49}\]  
\[ \begin{split}\textbf{R(Response)}=\forall\ i21\in x21\wedge i2 \in x22\mid(i2[1]=i2[1])\wedge\\ QueryResponse(x22^{\prime}:=x22\cup\{i22[3]\}).\end{split}  \tag{50}\]  
We assume that the adversary has the strength to capture location messages communicated to a location server. In Equation (51), the adversary can capture the location messages during communication as well as conspire with the location server to get vehicle location data. The adversary performs two things on location messages, namely, identity matching and location matching attack. In Equation (52), the adversary tries to compare a target vehicle's identities with different timestamps. However, in Equation (53), the adversary launches a location matching attack on vehicle location data. The adversary tries to match the various location traces of a target vehicle. \[ \begin{split}\textbf{R(Conspire)}=\forall\ i23\in x23\wedge i24 \in x24\wedge i25\in x25\mid Compare(i23[1],\\ i24[1],i25[1])\to Update(x25^{\prime}:=x25\cup\{i25[3],i25[4]\}). \end{split}  \tag{51}\]  
\[ \begin{split}\textbf{R(IDMatching)}=\forall\ i26\in x26\wedge i27 \in x27\wedge i28\in x28\mid(i26[1]\wedge i27[1])\\ \in i28[1]\wedge Match(i27[2],i28[2])=True\to x28^{\prime}:=x28\cup i28 [6].\end{split}  \tag{52}\]  
\[ \begin{split}\textbf{R(LOCMatching)}=\forall\ i29\in x29\wedge i3 0\in x30\mid(i29[1]=i30[1])\wedge\\ Match(i29[5],i30[5])=True\to x30^{\prime}:=x30\cup\{i30[6]\}). \end{split}  \tag{53}\]  
The adversary is trying to find the different locations visited by a target vehicle while the position-mixing algorithm hides the adversary's identities and locations. In the position-mixing method, the location requested messages contain the group identity and location coordinates of a neighboring vehicle that hides and mixes a target vehicle with its neighbor, this producing difficulty for an adversary to identify the target vehicle accurately.