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

 

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

 

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