# Virtual Pseudonym-Changing and Dynamic Grouping Policy for Privacy Preservation in VANETs
## 5 Formal Modeling and Specification
### Formal Modeling and Analysis of Attacker Scenario on Pseudonym-Changing Protocol
The selected members are verified, and each member starts the creation of the messages with different pseudonyms and location information, as stated in Equation (36). Finally, all the selected members of the group take part in the virtual pseudonym change process. The virtual update process is successfully done, as shown in Equation (37). \[ \begin{split}\textbf{R(VirtualPC)}=\forall\ i9\in x9\wedge i10\in x 10\mid(i10[1]\wedge i10[2]\in i9[2]\wedge i9[3]\\ <i9[4])\to SelectMembers(x10^{\prime}:=x10\cup\{i10[3],i10[4],i10[4]\}. \end{split}  \tag{35}\]  
\[ \begin{split}\textbf{R(Virtualizer)}=\forall\ i11\in x11\wedge i 12\in x12\wedge i13\in x13\mid(i11[2]\wedge i13[2]\\ \in i12[2])\to Verify\wedge PseudoCreation(x13^{\prime}:=x13\cup\{i13 [3],i13[4]\}.\end{split}  \tag{36}\]  
\[ \begin{split}\textbf{R(Pupdate)}=\forall\ i14\in x14\wedge i15 \in x15\mid(i15[1]\wedge i15[2]\in i14[2]\wedge i14[5]\\ =1)\to VirtualUpdate(x15^{\prime}:=x15\cup\{i15[3],i15[4],i15[5]\}. \end{split}  \tag{37}\]  
The primary purpose of both the usual pseudonym update and virtual pseudonym update processes is to anonymize the vehicles in a group. When all the group members change pseudonyms successfully, their pseudo-identities are mixed, making it difficult for an adversary to find a vehicle's identity and location traces on the road network. Equation (38) shows the anonymization of vehicles after the pseudonym-changing process. Figure 12: HLPN for adversary analysis on pseudonym-changing protocol. \[ \begin{split}\textbf{R(Anonymization)}=\forall\ i16\in x16\wedge i17\in x17 \wedge i18\in x18\mid(i16[5]\wedge i17[4])=0\\ \to\textit{Anonymized}\wedge\textit{BroadCast}(x18^{\prime}:=x18 \cup\{i18[1],i18[2],i18[3],i18[4],i18[5]\}).\end{split}  \tag{38}\]  
After anonymization, each vehicle broadcasts beacons with the new pseudonyms. An adversary has a low-cost transceiver to capture the beacons of vehicles given in Equation (39) and collects vehicle data during the beacons' broadcast. Based on the vehicle data, the adversary tries to collect two types of information about a vehicle. First, it collects the various location data and tries to match the old location to the vehicle's new location as specified in Equation (40). Secondly, in Equation (41), the adversary applies a linking attack to link an old pseudonym with a new pseudonym. \[ \begin{split}\textbf{R(BCapture)}=\forall\ i19\in x19\wedge i20\in x 20\mid(i20[1]\wedge i20[2]\in i19[2])\\ \wedge\textit{CollectVD}(x20^{\prime}:=x20\cup\{i20[3]\}.\end{split}  \tag{39}\]  
\[ \begin{split}\textbf{R(Traces)}=\forall\ i21\in x21\wedge i22\in x 22\mid(i22[1]\wedge i22[2]\in i2[1])\wedge\\ MatchTraces(x22^{\prime}:=x22\cup\{i22[4],i22[5]\}.\end{split}  \tag{40}\]  
\[ \begin{split}\textbf{R(PseudoLinking)}=\forall\ i23\in x23\wedge i 24\in x24\wedge i25\in x25\mid(i23[2]=i25[2]\\ \wedge i24[2]=i25[5])\wedge\textit{Linking}(i24[1],i25[1])\wedge x25 ^{\prime}:=x25\cup\{i25[3],i25[5]\}.\end{split}  \tag{41}\]  
The adversary collects vehicle data about location traces and pseudonyms of a vehicle. The pseudonym-changing protocol creates anonymization in the group that increases the confusion of an adversary about the vehicle's actual pseudonyms. The pseudonym-changing protocol makes it difficult for an adversary to identify a target vehicle in the vicinity.