Formal Analysis And Verification Of IoV Authentication Protocol Based On Model Checking

Vehicular Ad-Hoc Network(VANET)is a communication network in the field of Internet of Vehicles(Io V),aiming to provide safe and convenient services for transportation through vehicle-to-vehicle and vehicle-to-infrastructure communication.Since the communication between many nodes in VANET is based on open wireless channels,they may face various threats of cyber attacks in open network environment,and researchers have proposed various security protocols for this purpose to ensure the communication security of VANET.However,due to the powerful capabilities of network intruders and the complexity of the communication network environment,the security of many security protocols cannot be guaranteed.Therefore,security analysis of security protocols is the key to ensuring the security of the Io V.In this paper,we focus on the security of Io V authentication protocols,and select the DAS protocol used in Io V authentication scenarios as the main research object.We use model checking technique and its supporting tool SPIN to formally analyze and verify the protocol,identify the insecurity factors in the protocol and improve it,which plays an important role in ensuring Io V security.The main work and innovations of this paper are as follows.(1)Propose a formal analysis scheme of security protocol with timestamp.Based on the construction of the protocol agent model,a discrete time model including time variables,clock functions,and timer variables is introduced to describe the time factors in the protocol,a timestamp checking model is introduced to check the freshness of messages,and assertions that can be recognized by SPIN are used to represent the time related security properties of the protocol.This scheme is used to verify the classic protocol WMF,and the attack against the protocol is successfully found,which proves that the proposed scheme is effective and can be introduced into the security analysis of the Io V authentication protocol which contains timestamp.(2)Proposed protocol abstraction rules.The Trusted Authority(TA)and Road Side Unit(RSU)are abstracted into a whole structure,and the key VSK issued by TA to vehicle is abstracted into the shared key of TA and vehicle,while the hash function is abstracted into the public key of the unknown subject,which is beneficial to reduce the complexity of the protocol model to alleviate the state explosion problem.(3)Analyze,verify and improve the DAS protocol.On the basis of the previous two works,use Promela to build a protocol model;build an intruder attack message database and an atomic knowledge base,and divide the intruder’s attack capabilities into four categories:storing messages,learning knowledge,forging attack messages,and sending attack messages,the intruder’s behavior model is given and the algorithm description and model implementation are given;the assertion is used to indicate the fresh authentication of the DAS protocol;finally,the SPIN is used to verify the model,and it is successfully found that there is a replay attack which causes TA to authenticate the vehicle from an expired authentication message in the DAS protocol.According to the attack path of the DAS protocol,the reason for the attack on the analysis protocol is that the timestamp information in the authentication message sent by the vehicle is not encrypted,so that the intruder can update the timestamp without decrypting the ciphertext.The protocol is improved by putting the timestamp information into the ciphertext block of the authentication message.The improved protocol is verified by model checking,and the experimental results show that the improved protocol does not detect any attacks.