Title: Model-based verification of privacy preserving authentication protocol for VANETs
Authors: Brijesh Kumar Chaurasia; Shekhar Verma
ITM University, Gwalior – 474001, India.
Indian Institute of Information Technology-Allahabad, Deoghat, Jhalwa, Allahabad – 211012, India
Abstract: The paper presents the verification of a privacy preserving authentication protocol using a finite state model checker SPIN. Authentication of various entities, vehicles and road side units, is vital for accepting the authenticity of messages broadcast by them. These messages are critical and actions taken by vehicles are related to human life. The authentication protocol is a distributed and asynchronous in nature. In the present work, the correctness of the protocol is verified using SPIN and its structure is depicted using finite state and sequence diagram. The results indicate that the proposed protocol is correct and meet the requirements of VANET.
Keywords: VANETs; verification; PROMELA; unified modelling language; UML; privacy preservation; privacy protection; authentication protocols; finite state models; vehicular ad-hoc networks; vehicle communications; network security.
Int. J. of Information Technology, Communications and Convergence, 2012 Vol.2, No.2, pp.120 - 137
Available online: 11 Aug 2012