# Virtual Pseudonym-Changing and Dynamic Grouping Policy for Privacy Preservation in VANETs
## 5 Formal Modeling and Specification
### Formal Modeling of Dynamic and Virtual Pseudonym-Changing Scheme  
We formally define and analyze our proposed scheme DGVP in this section. The HLPN of the proposed DGVP scheme is shown in Figure 11, which contains details about the registration process, GH selection, vehicle grouping, and pseudonym-changing mechanisms. Table 2 includes a description of symbols used in the HLPN, while Table 3 describes the places used in the Petri nets. Figure 11: HLPN for DGVP scheme. Before joining the network, each vehicle must register with the Government Authority, i.e., TA. Each vehicle direct requests TA with their identity and LPN as given in Equation (7). TA verifies the vehicle data provided by the VRD authority in Equation (8). After the verification of a vehicle, TA provides certificates in Equation (9). \[ \begin{split}\textbf{R(Registration)}=\forall\ i2\in x2\wedge i3\in x 3\ |\ i2[1]\
eq i3[1]\wedge\\ x3^{\prime}:=x3\cup\{i2[1],i3[2],i3[3],i3[4]\}.\end{split}  \tag{7}\]  
\[ \begin{split}\textbf{R(Verify-Vdata)}=\forall\ i4& \in x4\wedge i5\in x5\ |\ (i4[1]=i5[1]\wedge i4[2]=i5[2])\\ &=Verified\to x5^{\prime}:=x5\cup\{i4[1],i4[2],i4[3]\}.\end{split}  \tag{8}\] \begin{table}
\begin{tabular}{l l} \hline \hline
**Symbol** & **Description** \\ \hline \(\varphi\) (Reg-Request) & \(P(V_{ID}\times LPN)\) \\ \(\varphi\) (TA) & \(P(V_{ID}\times LPN\times PU_{i,k}\times PR_{i,k})\) \\ \(\varphi\) (VRD) & \(P(V_{ID}\times LPN\times Verdeentials)\) \\ \(\varphi\) (OBU) & \(P(V_{ID}\times P_{ID}\times PU_{i,k}\times P\times CertExpire)\) \\ \(\varphi\) (Discard-Request) & \(P(V_{ID}\times LPN\times InvalidCredentials)\) \\ \(\varphi\) (Req-Certificate) & \(P(V_{ID}\times LPN\times ExpireCert\times RequireCert)\) \\ \(\varphi\) (PExpiry) & \(P(P_{ID}\times PITLimit\times Flag\times Certificate)\) \\ \(\varphi\) (GH) & \(P(P_{ID}\times G_{ID}\times LOC\times Flag)\) \\ \(\varphi\) (Grouping) & \(P(P_{ID}\times VLR\times T_{x}\times Certificate)\) \\ \(\varphi\) (ValidCert) & \(P(P_{ID}\times VLR\times T_{x}\times ValidCredentials)\) \\ \(\varphi\) (JoinGroup) & \(P(P_{ID}\times G_{ID}\times VLR\times T_{x})\) \\ \(\varphi\) (NF) & \(P(P_{ID}\times G_{ID}\times VLR\times T_{x}\times Dist\times Count)\) \\ \(\varphi\) (NT) & \(P(P_{ID}\times G_{ID}\times Count\times Thersh)\) \\ \(\varphi\) (RC) & \(P(P_{ID}\times G_{ID}\times Thersh\times Indicator)\) \\ \(\varphi\) (Notify) & \(P(P_{ID}\times G_{ID}\times Indicator\times AlertPC)\) \\ \(\varphi\) (PUpdate) & \(P(P_{ID}\times G_{ID}\times IndicatorS\times CP\times Flag)\) \\ \(\varphi\) (VPC) & \(P(P_{ID}\times G_{ID}\times T_{x}\times SelectNeigh)\) \\ \(\varphi\) (DistCalculation) & \(P(P_{ID}\times G_{ID}\times Dist(V_{i}\times V_{j}))\) \\ \(\varphi\) (Virtualizer) & \(P(P_{ID}\times G_{ID}\times MinDist)\) \\ \(\varphi\) (MessageScreation) & \(P(P_{ID}\times G_{ID}\times MSG_{1}\times MSG_{2})\) \\ \(\varphi\) (Pseudo-Update) & \(P(P_{ID}\times G_{ID}\times CP\times Flag)\) \\ \(\varphi\) (PseudoValidity) & \(P(P_{ID}\times T_{x}\times FIag\times TIimit)\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Symbols used in HLPN for DGVP scheme. \begin{table}
\begin{tabular}{l l} \hline \hline
**Symbol** & **Description** \\ \hline DistCalculation & Calculation of distance between vehicles \\ Discard-Request & Discard-request of a Vehicle with invalid credentials \\ GH & Group Head \\ Issue-Cert & Issuance certificate to vehicles \\ LPN & License Plate Number \\ NF & Neighbor Function \\ Notify & Notification in the group for pseudonym change \\ NT & Neighbor Threshold \\ OBU & On-Board Unit \\ PExpiry & Vehicle Pseudonym expiration \\ Pupdate & Pseudonym update process \\ PseudoValidity & The validity of Pseudonym for some time \\ RC & Ready for pseudonym change \\ Reg-Request & Request for vehicle registration to TA \\ Req-Certificate & Vehicle request for certification \\ ValidCert & Valid certificate \\ VTC & The virtual pseudonym change process \\ VRD & Vehicle registration data \\ TA & Trusted Authority \\ \hline \hline \end{tabular}
\end{table}