# 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

Table 3: Places used in HLPN for DGVP scheme. \[ \begin{split}\textbf{R(Issue-Cert)}=\forall\ i6\in x6\wedge i7\in x7 \mid Match(i6[1],i7[1])=True\\ \to x7^{\prime}:=x7\cup\{i7[2],i7[3],i7[4],i7[5]\}.\end{split}  \tag{9}\]  
In Equation (10), the TA discards the request of a vehicle with invalid credentials. The vehicle continuously checks the expiry of certificates. On the meeting certificate expiry condition as given in Equation (11), the vehicle requires another certificate because it cannot take part in communication in the network with an invalid certificate. For this purpose, the vehicle requests (Equation (12)) for another certificate. \[ \begin{split}\textbf{R(Verify-Fail)}=\exists\ i8\in x8\wedge i9 \in x9\mid(i8[1]\
eq i9[1]\wedge i8[2]\
eq i9[2])\\ =WrongCredentials\to x9^{\prime}:=x9\cup\{i9[3]\}.\end{split}  \tag{10}\]  
\[ \begin{split}\textbf{R(CertExpire)}=\exists\ i10\in x10\wedge i1 1\in x11\mid(i10[1]=i11[1]\wedge\\ i10[4]=Expire)\to Required(\{i11[3]\}).\end{split}  \tag{11}\]  
\[ \begin{split}\textbf{R(CertRequest)}=\exists\ i12\in x12\wedge i1 3\in x13\mid(i12[1]=i13[1]\wedge\\ Status(i12[4])=Required)\to Request(\{i13[1],i12[3],i12[4]\}).\end{split}  \tag{12}\]  
A pseudonym validity is checked in Equation (13); if a vehicle pseudonym has not reached its expiry period, it will continue to broadcast with a valid pseudonym. Otherwise, the vehicle will take another pseudonym from its pseudonym pool. For the change in pseudonym, the GH-selection process is taken in Equation (14). TA can verify the credentials of the GH vehicle in the selection process. Multiple vehicle data is sent to the TA for the GH selection, and one of the vehicles is selected as the GH randomly. In Equation (15), the vehicle with invalid credentials is discarded in the GH-selection process. \[ \begin{split}\textbf{R(ValidPseudo)}=\forall\ i14\in x14\wedge i15 \in x15\mid(i14[2]=i15[1]\wedge i14[4]\\ \
eq Expire)\to x15^{\prime}:=x15\cup\{i15[2],i15[3]\}.\end{split}  \tag{13}\]  
\[ \begin{split}\textbf{R(GH-Selection)}=\forall i16\in x16\wedge i1 7\in x17\wedge i18\in x18\mid(i16[1]=i17[1]\wedge i16[2]\\ =TimeExpire)\to Random(i18[1])\wedge x17^{\prime}:=x17\cup\{ assign(i17[2]),i17[4]\}.\end{split}  \tag{14}\]  
\[ \begin{split}\textbf{R(GHSelectionFail)}=\exists\ i19\in x19\wedge i2 0\in x20\mid(i19[1]=i20[1]\wedge\\ i19[4]=Invalid)\wedge Discard(x20^{\prime}:=x20\cup\{i20[3]\}).\end{split}  \tag{15}\]  
After the GH selection, the grouping of vehicles is started. The vehicles add a request to GH for joining the group, as given in Equation (16). The transmission range vehicles may take part in joining the group. The request may pass or fail depending on the verification of a vehicle. In Equation (18), the GH will prohibit a vehicle joining if it has invalid certificates or other credentials. If it has a valid certificate, the vehicle is allowed to join the group, as shown in Equation (17). In Equation (19) on joining the group, the GH will provide Group Identity (GID) to the vehicles. \[ \begin{split}\textbf{R(RequestJoining)}=\forall\ i21\in x21\wedge i 22\in x22\mid(i22[2],i22[3])\\ =InRange)\wedge Request(x22^{\prime}:=x22\cup\{i21[2]\}).\end{split}  \tag{16}\]  
\[ \begin{split}\textbf{R(RequestPass)}=\forall\ i23\in x23\wedge i24 \in x24\mid(i23[2],i23[2])\wedge(i24[2],\\ i24[3])\implies InRange\wedge(x24^{\prime}:=x24\cup\{i24[4]\to Valid\}. \end{split}  \tag{17}\]  
\[ \begin{split}\textbf{R(RequestFail)}=\exists\ i25\in x25\wedge i26 \in x26\mid(i25[1]\in i26[1]\wedge\\ i25[4]=Invalid)\wedge Discard(x26^{\prime}:=x26\cup\{i26[3]\}).\end{split}  \tag{18}\]  
\[ \begin{split}\textbf{R(GroupJoining)}=\forall\ i27\in x27\wedge i28 \in x28\mid Compare(\{i27[2],i27[3]\}\wedge\\ (i28[3],i28[4]))\implies InRange\to AssignID(x28^{\prime}:=x28\cup\{i28[2]\}). \end{split}  \tag{19}\]After group formation, the neighbor function (NF) is used to count the number of vehicles in the group as specified in Equation (20). The NF will calculate the number of transmission range neighbors in the group.