ABSTRACT
In this chapter, we consider safety issues arising in vehicular ad hoc networks (VANETs) (Figure 3.1). Although vehicular networks originated in the infotainment domain, today they are also used in many safety-critical systems such as in an emergency vehicle grid. Due to the open nature of vehicular networks,
they are more amenable to malicious attacks; and, due to their high mobility and dynamic topology, the detection and prevention of such attacks is also more difficult. We consider one such attack in this chapter, the Sybil attack, in which an attacker tries to violate the unique vehicular ID property by forging or fabricating it and presenting multiple identities. A Sybil attack is a serious threat because it can result in large-scale denial of service or other security risks in the network. This chapter presents a new method to prevent Sybil attacks in a vehicular network based on the traditional cryptographic techniques, as well as the unique features of the network. A key feature of the methodology is the use of fixed roadside units and a central authority. This chapter presents a formal model of the system using the Promela language and shows how the safety property can be verified using the SPIN model checker.
