# A Distributed Mix-Context-Based Method for Location Privacy in Road Networks
## 5 Formal Modeling and Specification  
High-Level Petri Nets (HLPN) is used for two reasons [65]: to simulate the proposed model and provide mathematical representation for analyzing the proposed model's behavior and structure properties. Formal modeling benefits are the interconnection of system components and processes, information flow among the processes, and information processing. We used HLPN for formal modeling and specification of the proposed scheme. HLPN is a set of seven tuples \((P,T,F,\varphi,R,L,M_{0})\) as defined in [66]. In this section, we formally model and specify the proposed scheme CMC. We present the CMC scheme in HLPN in terms of mathematical properties (rules). For the representation of the system in HLPN, we define places and their associated data types; then, we specify a set of rules used in HLPN. Tables 2 and 3 contain details of the symbols and places used in the Petri nets. We design HLPN for Algorithms in the proposed model. Figure 8 shows the HLPN for the mix context scheme. The vertical bar shows transitions, and the circle shows places used in HLPN. The arrowheads in the diagram show the data flow in HLPN. Figure 7: Virtual pseudonym exchange process between two vehicles. \begin{table}
\begin{tabular}{l l} \hline \hline
**Symbol** & **Description** \\ \hline Reg-Request & Request for vehicle registration to TA \\ VRD & Vehicle registration data \\ AssignPool & Assign pseudonym pool to vehicles \\ PL & Pseudonym list \\ SM & Speed monitor \\ DC & Distance calculation \\ NS & Neighbor selection \\ NC & Neighbor count \\ NT & Neighbor threshold \\ SameID & Same vehicle (only one vehicle) \\ RC & Vehicle ready to change pseudonym \\ CPC & The cooperative pseudonym change process \\ ExpiryT & Pseudonym expiry time \\ PEP & Pseudonym exchange process \\ TNN & Transmission range neighbors \\ RSN & Random selection of neighbors \\ PE & Pseudonym exchange \\ BC & Broadcast beacon messages \\ LPN & Vehicle license plate number \\ \(V_{ID}\) & Vehicle identity \\ \(P_{ID}\) & Pseudo IDs of a vehicle \\ WT & Waiting time \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Symbol description used in the mix-context method. \begin{table}
\begin{tabular}{l l} \hline \hline
**Types** & **Description** \\ \hline \(\varphi\) (Reg-Request) & \(P(V_{ID}\times LPN)\) \\ \(\varphi\) (VRD) & \(P(V_{ID}\times PK_{p}\times P)\) \\ \(\varphi\) (Pseudo-Request) & \(P(V_{ID}\times LPN)\) \\ \(\varphi\) (PL) & \(P(P_{ID}\times PK_{p}\times P)\) \\ \(\varphi\) (Road-Condition) & \(P(SP_{R}\times D\times T_{x})\) \\ \(\varphi\) (SM) & \(P(P_{ID}\times SP\times SP_{R}\times D)\) \\ \(\varphi\) (DC) & \(P(P_{ID}\times POSV_{i}\times POSV_{j}\times Dist)\) \\ \(\varphi\) (NS) & \(P(P_{ID}\times T_{x}\times Neigh)\) \\ \(\varphi\) (NC) & \(P(P_{ID}\times Dist\times NeighC)\) \\ \(\varphi\) (NT) & \(P(P_{ID}\times NeighC\times Dist\times Flag)\) \\ \(\varphi\) (SameID) & \(P(P_{ID}\times Dist)\) \\ \(\varphi\) (RC) & \(P(P_{ID}\times N_{ID}\times Threshold\times Indicator)\) \\ \(\varphi\) (CPC) & \(P(P_{ID}\times N_{ID}\times IndicatorS)\) \\ \(\varphi\) (PUpdate) & \(P(P_{ID}\times WT\times Flag)\) \\ \(\varphi\) (ExpiryT) & \(P(P_{ID}\times ThreshT\times WT\times Flag)\) \\ \(\varphi\) (PEP) & \(P(P_{ID}\times N_{ID}\times Thresh\times Indicator)\) \\ \(\varphi\) (\(T_{x}N\)) & \(P(P_{ID}\times N_{ID}\times IndicatorS\times RSN)\) \\ \(\varphi\) (PE) & \(P(P_{ID}\times N_{ID}\times Msg_{i}\times Msg_{j})\) \\ \(\varphi\) (BC) & \(P(P_{ID}\times Msg_{i}\times Msg_{j})\) \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Places used in HLPN for mix-context method. The vehicle must register with TA before joining the network. For this purpose, the vehicle requests TA for registration. The TA processes the demand and provides Public Key \((PK_{\text{v}})\) and pseudonyms \((P)\) in Equation (1). In Equation (2), a vehicle requests a pseudonym pool if it has expired. To assign the pseudonym pool to a vehicle, the vehicle's identity is verified, and the pseudonym pool is assigned to a vehicle as given in Equation (3).