Internet of Vehicles Environment Verification of Authentication Protocols using Formal Analysis: A Survey

The Internet of Vehicles (IoV) is becoming an interesting topic among researchers and it has emerged as a rapidly advancing field within Vehicular Ad-hoc Networks, facilitating intelligent communication between vehicles and the cloud through the integration of Internet of Things (IoT) technologies. The IoV surroundings face serious challenges due to the highly interrelated nature of vehicles and infrastructure in certifying privacy and security. Traditional approaches to authentication lack the strength required to protect against developing fears, leaving systems vulnerable to attacks. This survey addresses the gap by employing formal analysis approaches to prove authentication protocols, targeting to reinforce safety and confidentiality in IoV systems. The IoV communication model consists of Vehicle-to-Vehicle, Vehicle-to-Infrastructure, Vehicle-to-Personal Devices, and Vehicle-to-Cloud. Smart automobiles are equipped with cameras, radars, on-board units, and sensors to help reduce the number of accidents by giving drivers or autonomous vehicles up-to-date information on roads, traffic signals, and other pertinent entities. As human lives are at risk, security and privacy in the IoV communication paradigm are critical and cannot neglected. Security and privacy breaches may cause accidents because the attacker can inject false information into the system as the communication channel is open and unsecured. The researchers proposed many authentication protocols to provide secure communication between IoV entities. Although surveys on IoV security and privacy issues deal with communication and computation costs, they lack formal analysis of the authentication protocols. This survey reviews the informal analysis and formal analysis methods used by various authentication protocols. Furthermore, the challenges and future work are also included in this survey.