Modeling and Verifying Privacy-Preserving Authentication Scheme for VANET Using CSP

As an important part of intelligent traffic, Vehicle Ad hoc Network (VANET) is extensively applied which can provide secure communication mechanisms. Due to the necessity of security in VANET, a privacy-preserving mutual authentication scheme was proposed to ensure secure communication for the entities, however, this scheme has not been verified from the formalization view. In this paper, we propose and formally model the privacy-preserving mutual authentication scheme with the man-in-middle attack using Communication Sequential Process (CSP). Five properties are defined and verified including data availability for components, conditional privacy preservation, data confidentiality, data integrity and traceability based on the Process Analysis Toolkit (PAT). Initially, the results of verification indicate that this scheme cannot satisfy data confidentiality, data integrity and traceability. To enhance the security mechanism, two improved approaches are proposed to support the security of this scheme, which adopt the special encryption strategy and change the original checksum. The results of the new verification show that all properties are satisfied and the secure communication is guaranteed.