# 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  
We formally model and analyze the adversary scenario on the pseudonym-changing protocol. Figure 12 shows the HLPN for the attacker scenario that consists of two entities, i.e., pseudonym-changing protocol and an adversary. The symbols used in HLPN are described in Table 4, while the places used in Petri nets are shown in Table 5. The first transition input is taken from the neighbor function and put into place NT. The input transition contains data about vehicle neighborhoods, such as the number of transmissions range neighbors, the status of vehicle pseudonyms, group information, and group identity. NT in the Petri net takes input the number of neighbors for satisfying the neighbor threshold. In Equation (32), the neighbor threshold is met, and the concerned pseudonym update process is started. \begin{table}
\begin{tabular}{l l} \hline \hline
**Symbol** & **Description** \\ \hline BCapture & Capturing of beacon messages \\ CP & Change pseudonym \\ Identification & Identification of a vehicle by an adversary \\ NT & Neighbor threshold \\ NeighAlert & Alert neighbors for the pseudonym change process \\ \(NP_{ID}\) & New pseudo-identity \\ OldPseudo & Old pseudonyms of a vehicle \\ PCC & Pseudonym change collectively \\ PC & Pseudonym change \\ Pseudo-IDs & Vehicle pseudo-identities \\ ReadyNeigh & Neighbor vehicles ready for pseudonym change \\ TS & Timestamp \\ TxNeigh & Transmission range neighbors \\ VD & Vehicle data \\ VirtualPC & Virtual pseudonyms change process \\ \hline \hline \end{tabular}
\end{table} 
Table 4: Symbols used in HLPN for attacker scenario in DGVP scheme. \begin{table}
\begin{tabular}{l l} \hline \hline
**Symbol** & **Description** \\ \hline \(\varphi\) (NT) & \(P(P_{ID}\times G_{ID}\times Count\times Thresh)\) \\ \(\varphi\) (PC) & \(P(P_{ID}\times G_{ID}\times Thresh\times CPC)\) \\ \(\varphi\) (GH) & \(P(P_{ID}\times G_{ID}\times LOC\times Flag)\) \\ \(\varphi\) (NeighAlert) & \(P(P_{ID}\times G_{ID}\times Indicator\times AlertPC\times Flag)\) \\ \(\varphi\) (Pseudo-Update) & \(P(P_{ID}\times G_{ID}\times PCC\times Flag)\) \\ \(\varphi\) (TxNeigh) & \(P(P_{ID}\times G_{ID}\times T_{x}\times NS\times Dist(V_{i}\times V_{j}))\) \\ \(\varphi\) (Pseudo-IDs) & \(P(P_{ID}\times G_{ID}\times MSG_{1}\times MSG_{2})\) \\ \(\varphi\) (Updation) & \(P(P_{ID}\times G_{ID}\times SkipVP\times CP\times Flag)\) \\ \(\varphi\) (Beacons) & \(P(NP_{ID}\times G_{ID}\times LOC\times S\times D)\) \\ \(\varphi\) (VD) & \(P(NP_{ID}\times G_{ID}\times collect(P_{ID},LOC))\) \\ \(\varphi\) (Identification) & \(P(NP_{ID}\times G_{ID}\times Odd_{ID}\times OldTraces\times CLOC)\) \\ \(\varphi\) (OldPseudo) & \(P(OldP_{ID}\times LOC\times TS)\) \\ \hline \hline \end{tabular}
\end{table} 
Table 5: Places used in HLPN for attacker scenario in DGVP scheme. A pseudonym-changing alert is disseminated if vehicles are in the same group (Equation (33)). All vehicles become ready for pseudonym change. In Equation (34), the pseudonym updating process is started, and vehicles change pseudonyms collectively to anonymize pseudo-identities in the group. This creates confusion for an adversary trying to identify the target vehicle. \[ \begin{split}\textbf{R(Satisfy)}=\forall\ i2\in x2\wedge i3\in x3 \mid(i2[2]=i3[2]\wedge i3[4]=Threshold)\\ \wedge Notify(x3^{\prime}:=x3\cup\{i3[4]\}.\end{split}  \tag{32}\]  
\[ \begin{split}\textbf{R(ReadyNeigh)}=\forall\ i4\in x4\wedge i5 \in x5\wedge i6\in x6\mid(i4[2]\wedge i6[2]\in i5[2]\\ =SameGroup)\to GHAlett(x6^{\prime}:=x6\cup\{i6[3],i6[4],i6[5]\}. \end{split}  \tag{33}\]  
\[ \begin{split}\textbf{R(Updating)}=\forall\ i7\in x7\wedge i8\in x 8\mid(i8[1]\wedge i8[2]\in i7[2]\wedge i7[5]=1)\\ \to CollectiveUpdate(x8^{\prime}:=x8\cup\{i8[3],i8[4]\}.\end{split}  \tag{34}\]  
If the neighbor threshold is not satisfied, then the virtual pseudonym change process is started as specified in Equation (35). The GH selects a few members for a pseudonym update process.