# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
## 2 Related Work
### Message Dissemination and Authentication Scheme  
In [16], the automobiles are classified into clusters based on their driving directions. The information processing for each cluster is the responsibility of the cluster head. The bring and forward scheme is used by nodes that receive the emergency call. According to simulation results, the packet propagation ratio rises as the number of nodes rises. To facilitate the use of Long-Term Evolution (LTE) networks in data transfers, many strategies for managing VANETs have been proposed. Clustering cars and organizing the network through clusters is one of the most general and successful approaches [17]. In this paper, the authors introduce an algorithm for disseminating reports about real-time traffic situations in VANETs. Using this process, each vehicle decides when to distribute reports, how many to distribute, and which reports are distributed on a local level [18]. The authors propose a distributed clustering-based vehicle-to-roadside communication protocol, in which vehicles join clusters using a coalitional game approach, and stable clusters are built using a fuzzy logic algorithm based on multiple metrics of vehicle velocity, moving pattern, as well as signal quality between vehicles. Each vehicle is guided by a reinforcement learning system that uses game theory to determine the most efficient path for overall network performance [19]. Vehicles are grouped with sensors, as well as sinks are placed along the path to collect or/and transmit data to the sensor, according to a draft authentication protocol for an autonomous vehicle system. The customer keeps track of the vehicles by gathering data from sinks with analyzing it before acting [20]. The transmitting of messages in an open-access environment, such as the VANET, raises the most serious and difficult security concerns. Protection in the VANET includes authentication, data confidentiality, data privacy, data availability, and nonrepudiation. The authentication schemes in VANET are adopted because they play a vital role in safe communication. The major task of the paper is to include a taxonomy of authentication systems, as well as to review their methods, benefits, drawbacks, efficiency, and scope [21]. The authors suggest a randomized authentication protocol based on homomorphic encryption that allows each vehicle in a VANET to create any number of authenticated identities in order to achieve complete anonymity. According to the suggested protocol, cars, including peer vehicles, transportation services, authentication servers, and other devices, cannot be managed by a single entity [22]. In this paper, the existence of resource-constrained nodes should be addressed by a robust authentication approach. To achieve both of these goals, the authors propose a lightweight multi-factor authentication and privacy-preserving protection solution for VANETs. It employs a combination of physically unclonable functions (PUF) and one-time complicated pseudo-identities as authentication variables. Apart from this, by decentralizing the certificate authority's (CA) wide precinct into regional domains as well as gaining comprehensive control of domain keys, it removes the strong reliance on the device key [23].