Authentication is an essential security requirement in safety-related vehicle-to-vehicle applications in VANETs. TESLA is one of the most popular broadcast source authentication protocols proposed and standardized for this purpose. Having strict time constraints and being prone to GPS synchronization errors make the analysis of this protocol challenging. In this paper, we utilize a timed model checking approach based on timed colored Petri nets to model and verify TESLA considering its time-sensitive behaviors. In this way, we show how neglecting timing aspects in protocol design and in protocol modelling can lead to successfully launched attacks and erroneous analyses respectively, and how its refinement can help improve the protocol’s security.
Our work extends the problem of analyzing basic TESLA done in previous related works, to one in which TESLA is modelled and verified in a loose synchronization setting, which is the case in VANETs. This new problem definition led to finding new attacks that are directly rooted in the sending times of packets. We show what changes need to be made to TESLA so that its security property be preserved in a loose synchronization condition.