Int. J. of Information Technology, Communications and Convergence   »   2012 Vol.2, No.2



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.


DOI: 10.1504/IJITCC.2012.048481


Int. J. of Information Technology, Communications and Convergence, 2012 Vol.2, No.2, pp.120 - 137


Available online: 11 Aug 2012



Editors Full text accessAccess for SubscribersPurchase this articleComment on this article