Title: Model-based verification of privacy preserving authentication protocol for VANETs

Authors: Brijesh Kumar Chaurasia; Shekhar Verma

Addresses: 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

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

Published online: 16 Aug 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article