Sybil attack detection technique using session key certificate in vehicular ad hoc networks

Sybil attack prevention and detection in vehicular ad hoc network Sybil attack detection in vehicular network based on received signal strength
Dr.MohitBansal Profile Pic
Published Date:26-10-2017
Your Website URL(Optional)
Sybil Attack Detection in Vehicular Networks (VANETs) (Figure 3.1). Although vehicular networks originated in the infotain- ment 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, 3536  Security and Privacy in Internet of Things (IoTs) Central authority Roadside unit Roadside unit Roadside unit Figure 3.1: Architecture of vehicular ad hoc network 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 dif- ficult. 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 net- work 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. 3.1 Introduction The automobile today has evolved from a complex electromechanical system to a “computer system on wheels” and vehicular networks are pushing the frontierSybil Attack Detection in Vehicular Networks  37 of the internet of things (IoT) to include the large class of highly mobile entities; namely, vehicles. With the inclusion of vehicles and communication between vehicles, as well as between vehicles and the infrastructure, the “internet of vehi- cles” can potentially provide real-time connectivity between vehicles around the globe. By further providing connectivity with entities such as traffic lights and RFID devices, we move closer toward the goal of a safe and efficient traffic environment. A vehicle has potentially has more storage, communica- tion, and computing capacity compared to other embedded and mobile devices, and hence, vehicular networks can act as core infrastructure to connect various things. The vehicular ad hoc network (VANET) facilitates communication between vehicles in the network by sharing road conditions and safety information. The network is especially useful in dense urban regions in promoting greater road safety and efficient traffic control. In contrast with a mobile ad hoc network, a vehicular ad hoc network has a highly dynamic network topology owing to the rapid movement of vehicles, with frequent disconnections in the network and more resource constraints 13. It uses a combination of networking technolo- gies such as Wi-Fi IEEE 802.11p, WAVE IEEE 1609, WiMAX IEEE 802.16, Bluetooth, IRA, and ZigBee. There are two types of communication in a vehicular network: (i) vehicle-to- vehicle and (ii) vehicle-to-network-infrastructure. The open nature of VANET communication makes it much more amenable to malicious attacks 11, 18, and the dynamic nature of vehicular movement makes it difficult to pro- tect against these. In this chapter, we consider one such attack, the Sybil attack, in which a single entity can gain control over a substantial fraction of the system by presenting multiple identities 4. There are mainly two types of Sybil attacks: (i) a single node presents multiple identities; and (ii) a Sybil node uses the identity of another node. Sybil attacks violate the funda- mental assumption of one-to-one correspondence of a node with its identity. There are several adverse effects that result from a Sybil attack in a VANET environment 1, 14:  Routing: The Sybil attack affects the performance of geographical rout- ing and leads to large-scale denial of service.  Tampering with voting and reputation systems: Reputation and trust man- agement system crucially depend upon the unique ID and authenticity of the node. A Sybil attack violates this assumption and results in erroneous computation of reputation values.  Fair resource allocation: A node with multiple identities can exploit the network to its advantage by using more bandwidth and network time.38  Security and Privacy in Internet of Things (IoTs)  Data aggregation: Wireless sensor networks typically aggregate the val- ues from sensor nodes rather than sending individual values. A Sybil node can manipulate these values, resulting in misleading aggregate values. Our motivation in this chapter is to present an effective approach for Sybil attack detection in the setting a highly dynamic vehicular ad hoc network. Basi- cally, a Sybil attack can be prevented by using public key certificates issued by a central authority (CA) 4. Such an approach is not scalable because the CA can become a bottleneck in communication. Although methods have been pro- posed to prevent a Sybil attack in a VANET 2, 10, 15, they fail to capture the dynamic characteristics of the network. Our method makes use of the roadside unit (RSU) along with a cryptographic certificate scheme with position verifica- tion to capture the dynamic context of a vehicle in the network. Essentially, in our approach, the RSU acts as an authority to verify the authenticity of a vehi- cle node by using the information in nearby RSUs. The idea is that an RSU can contact nearby RSUs more quickly compared with the CA. Thus, the contribution of our work is an effective detection mechanism for Sybil attacks, using a semicentralized approach, by taking advantage of the presence of RSUs in addition to the CA. Essentially, we distribute the function performed by the CA through the RSUs to capture the dynamic nature of the net- work. A real vehicular network typically contains thousands of vehicular nodes and hundreds of RSUs. Before deploying the system in a real environment, it is desirable to model the key aspects of the technique at an abstract level and check the correctness of the proposed protocol. We therefore develop a formal model of our approach and verify its key properties using a model-checking approach 3, since it supports reasoning over all possible paths of execution. We develop a specification of the vehicular network using Promela (Process Meta Language) and check its correctness using the open-source model checker SPIN (Simple Promela Interpreter) 6. Vehicles, RSUs, and the CA are mod- eled as Promela processes, and the communication between them is represented by Promela channels. Promela supports the dynamic creation of processes as well as channels, the latter being a crucial capability for modeling the mobil- ity of vehicles from one RSU to another. Attack detection is also modeled as a process that continuously observes the network for any violation of the key sys- tem properties, including the property that only one vehicle uses a given ID for communication. The remainder of this chapter is organized as follows: Section 2 presents closely related approaches for Sybil attack detection and their limitations; Section 3 presents the overall design of our Sybil attack detection method; Section 4 gives a formal specification and verification of our method using Promela/SPIN; and Section 5 presents conclusions and areas of further work. The full Promela model is given in the appendices.Sybil Attack Detection in Vehicular Networks  39 3.2 Related Work A Sybil attack can cause harm to various layers of communication 7, 16. In this section, we discuss the methods that have been proposed for different network scenarios. Newsome et al. 8 propose a detection scheme based on resource testing for wireless sensor networks, assuming that each entity has limited resources. According to this approach, communication capability is used for resource test- ing. The principle here is that radio is incapable of simultaneously sending or receiving on more than one channel. If a node wants to verify its neighboring nodes, it will assign each of its neighbors to a different channel to broadcast messages. The verifier node then randomly selects a channel to listen to. If it receives the message on the assigned channel, then it is a legitimate node; other- wise it is a Sybil node. But an attacker can, in practice, use unlimited resources or radios to launch an attack. Douceur 4 notes that a Sybil attack can be effectively prevented using public key certificates issued by a CA. However, due to the dynamic nature of VANET, it is impractical to communicate with a CA each time. Also, in this method, an attacker can easily use a stolen certificate for communication because there is no certificate binding with a unique physical identification. Zhou et al. 19 proposed a scheme to preserve privacy based on pseudonyms. Here, each vehicle has a set of pseudonyms issued by the Department of Motor Vehicles (DMV). For each communication, a vehicle uses one of its pseudonyms rather than its real ID. Pseudonyms in vehicles are hashed to a unique value, and hence cannot be used to launch a Sybil attack. This scheme needs a lot of communication with the central authority for pseudonym verification, making it less practical in the highly dynamic context of a vehicular network. Park et al. 10 suggest a scheme based on the time-series approach. Here, each vehicle-to-vehicle communication contains a unique time series certificate certified by the RSU. This method is based on the basic assumption that it is not possible for two vehicles to pass through the same RSU at same time. A vehicle can detect a Sybil attack when it receives a similar certificate from a different vehicle. This method can identify a Sybil attack to some extent, but here, attack detection occurs at the vehicle level. This scheme is based on the dense deploy- ment of RSUs. This method is applicable only if both the Sybil node and the actual node are within the range of the same RSU. The position verification scheme 12 is an another approach to detect a legit- imate node. It is based on the assumption that a vehicle can be present at only one position at a particular time. Yan et al. 17 presented an approach for position verification using onboard radar at a node to verify the location of a neighboring vehicle. Here, each vehicle sends a message with location information. A vehi- cle can cross-check the presented location information using onboard radar, but location verification is limited by its range.40  Security and Privacy in Internet of Things (IoTs) According to Guette et al. 5, secure hardware built on a trusted platform (TPM) can be used to prevent Sybil attacks in a VANET. Secure information is stored in the TPM; hence, forging and fabrication of data is impossible. Creden- tials are trusted by car manufacturers and the communication between two TPMs are protected from attack. 3.3 Location Certificate-Based Scheme Our proposed approach for Sybil attack detection is based on a traditional public key certificate together with position verification. In this approach, the whole network is viewed as a tree-like structure rooted at the CA, which maintains information about all vehicles in the VANET. At the second level, or layer, from the root is the set of all RSUs, which effectively constitute a fixed infrastructure. Unlike a normal tree structure, there are links between RSUs. The third (and last) level from the root contains the mobile nodes (vehicles). Each vehicle has a unique ID and certificate registered with the CA. The main properties of the proposed design are as follows:  No dependence on specialized hardware: This scheme does not need any special type of hardware. It makes use of existing infrastructure for the detection of attacks.  The CA and RSUs both participate in detection: This approach avoids a central bottleneck in communication, and attack detection happens at both the CA and RSU levels. The support of other vehicles in the network is not needed.  Node authentication depends on geolocation information: The claimed location of nodes is verified using the strength of received signals and also the geographic location of nodes.  Support for high vehicular mobility: Our proposed approach supports a high mobility of vehicles between RSUs. The overhead associated with attack detection does not affect the performance of the VANET.  Sybil nodes are isolated from the network: The Sybil node will be auto- matically removed from the network and will be prevented from engaging in any further communication. The fundamental assumptions for the proposed scheme are as follows: (i) Each RSU must know its geographical location. (ii) The RSUs are connected to adjacent RSUs and the CA with a high-speed back end. (iii) RSUs are considered as trusted entities. (iv) Each vehicle is registered with the CA with a unique ID and public key certificate. (v) Each vehicle has a GPS device to acquire its geolocation.Sybil Attack Detection in Vehicular Networks  41 Position verification encrypt (M=Vid, position, –1 V timestamp, sign (M, PKV ), j j RSU i PKRS ) i Figure 3.2: Communication from vehicle to RSU 3.3.1 Sybil node detection scheme Our proposed scheme is founded on the concept of a location certificate issued by a RSU for communication with other vehicles under the same RSU. For each vehicle j, the CA stores the vehicle ID with the corresponding public key (PKVj). Each RSU continuously broadcasts its public key (PKRS) using the beacon signal. Before we describe the major steps in this scheme, we first clarify the common notations used in this scheme in the table below. Notation Meaning −1 (PKCA,PKCA ) Public and private key of CA −1 (PKRS ,PKRS ) Public and private key of ith RSU unit i i −1 (PKV ,PKV ) Public and private key of jth vehicle j j 1. Suppose the jth vehicle enters the ith RSU’s range (Figure 3.2). This step is a one-time process for each session and occurs only if the vehicle does not have a valid location certificate. The vehicle creates a location certifi- cate request in the following format: vehicle ID, position, timestamp. Here, position is taken from the GPS sensor. For communication secu- −1 rity, a message is signed using the vehicle’s private key, PKV , and j encrypted by the ith RSU’s public key. 2. When obtaining a location request from the jth vehicle, the RSU first ver- ifies the claimed position using the received signal strength (RSS), since it is possible to calculate the distance from a node using the RSS 9. If it is valid, the RSU forwards the encrypted request to the CA using PKCA (Figure 3.3). If the claim of the vehicle is invalid, the RSU notifies the vehicle ID to adjacent RSUs. 3. The CA verifies the request using PKV and checks if the jth vehicle is j registered anywhere in the network. If it is not, it registers the vehicle loca- tion with the RSU and notifies the corresponding RSU using the vehicle’s PKV (Figure 3.4). The CA knows the public key of all RSUs and hence j can securely communicate with RSUs.42  Security and Privacy in Internet of Things (IoTs) CA encrypt (M=Vid, position, –1 RSU timestamp, sign (M, PKV , i j PKCA) Figure 3.3: Communication from RSU to CA CA encrypt (M=PKV , Vid, PKRS ) j i RSU i Figure 3.4: Communication from CA to RSU encrypt (M=rsu_id, Vid V rsu_shared_key, expiry_time, j RSU i PKV ) j Figure 3.5: Communication from RSU to vehicle 4. After obtaining the confirmation from the CA, the RSU issues a location certificate with rsu ID, rsu shared key, vehicle ID, expiry time which is encrypted with the vehicle’s public key (Figure 3.5). If the CA detects a Sybil attack, it will inform the RSU concerned, which in turn will not issue a certificate to the vehicle. 5. A particular vehicle communicates with other vehicles using an rsu shared key. Each vehicle continuously checks the expiry time of the location certificate and sends a location certificate request before the expi- ration of the previously issued certificate. The valid location certificate acts as a key for vehicle-to-vehicle communication. 6. If a vehicle enters the range of the next RSU, it again sends a location cer- tificate request to the RSU, but it includes the position certificate from pre- vious RSU (Figure 3.6). When the kth RSU gets a request with a position certificate from the ith RSU, it checks the validity of the certificate from the ith RSU and acquires the public key of the corresponding vehicle. The kth RSU then issues the certificate and notifies the CA of the vehicle ID and rsu ID. Subsequently, the ith RSU removes the corresponding vehicle from its storage.Sybil Attack Detection in Vehicular Networks  43 Position verification encrypt (M=Vid, position, V j timestamp, loc cert, RSU k –1 sign (M, PKV ), PKRS ) j k Figure 3.6: Communication from vehicle to RSU with previous location certificate Evaluation. In this scheme, the Sybil node detection happens at two lev- els. Each RSU can verify the node (vehicle) based on location information, and the CA can check whether the node registration occurred anywhere in the net- work using a unique ID. An attacker cannot send a legitimate request to the CA, since the CA can check the validity of the message using the vehicle’s public key. Each RSU requires less storage space because it stores information only of those vehicles that are within its range—an RSU erases a vehicle’s details after it moves to the next RSU. Without a location certificate, vehicles cannot com- municate with other vehicles and this prevents a Sybil node from taking part in further communication. If an RSU or the CA detects a Sybil attack, it informs nearby RSUs, which in turn can reject a vehicle request without going through the remaining process. 3.4 Formal Modeling and Verification Formal verification is a method to check various system properties such as live- ness, deadlock, and design errors. SPIN is a powerful tool to conduct formal verification of concurrent systems using specifications in Promela, a process specification language. We model the location certificate distribution method without considering the cryptographic processes involved with it. Here the CA, RSUs, and vehicles are modeled as a Promela proctype. The system has multiple instances of RSUs and vehicles. Communication between these processes occurs through Promela channels. Each RSU maintains, for vehicle communication, a certificate request channel (veh rsu chan) and a certificate response channel (rsu veh chan). These channels are asynchronous and defined as chan veh_rsu_chanNO_OF_RSU+1=0 of CER_REQ; chan rsu_veh_chanNO_OF_RSU+1=0 of CER_RES; The types CER REQ and CER RES represent, respectively, the certification request from a vehicle and the response from the RSU. A location certifi- cate request contains the vehicle identity (veh ID), vehicle location (veh loc), request time, and available location certificate. The initial RSU ID is supplied by the initialization process. Vehicle movement is achieved by changing RSU IDs and locations. These structures are defined through Promela typedefs (Figure 3.7).44  Security and Privacy in Internet of Things (IoTs) Proctype CA CA_RSU_CHAN1 CA_RSU_CHAN2 RSU_CA_CHAN RSU_REQ_CHAN2 Proctype RSU1 Proctype RSU2 RSU_RES_CHAN1 VEH_RSU_CHAN1 RSU_VEH_CHAN1 VEH_RSU_CHAN2 VEH_RSU_CHAN2 Proctype Proctype Proctype Proctype Vehicle1 Vehicle2 Vehicle3 Vehicle4 Figure 3.7: Promela channels and process types typedef CER_REQ byte veh_ID; byte veh_loc; byte rsu_ID; int loc_cert; int time; typedef CER_RES byte veh_ID; byte rsu_ID; int loc_cert; The typeloc cert contains a positive value for a valid certificate. After obtain- ing a valid certificate from the RSU, the vehicle process increments the RSU ID by one and tries to associate with it using the current location certificate. The vehicle proctype is detailed in Appendix 3A.1. The RSU uses two other channels to communicate with the CA: one for communication from the RSU to the CA (rsu ca chan) and the other from the CA to the RSU (ca rsu chan). chan rsu_ca_chan=0 of RSU_REQ; chan ca_rsu_chanNO_OF_RSU+1=0 of CO_RES According to the proposed scheme, the RSS (received signal strength) method is used at each RSU for location verification. It is difficult to model such an environment in SPIN. Therefore, here we are using a simpler method for location verification. The RSU checks that the location is within a 4 km range of the RSU. If this is so and the request contains an invalid certificate, then the RSU forwards it to the CA using theRSU REQ data structure. typedef RSU_REQ byte veh_ID; byte rsu_ID; bit update; Theupdate field inRSU REQ is set to zero for a request with an invalid certificate. If a request from a vehicle contains a valid certificate, the request is forwarded to the RSU which issued the current certificate. To communicate with nearby RSUs, each RSU maintains a request and response channel. chan rsu_req_chanNO_OF_RSU+1=0 of CER_REQ,byte chan rsu_res_chanNO_OF_RSU+1=0 of CO_RESSybil Attack Detection in Vehicular Networks  45 Here,CO RES is the common response format of an RSU: typedef CO_RES byte veh_ID; bit status; After receiving a positive request from a nearby RSU or the CA, the RSU issues the new certificate through thecer res chan channel. To update the certificate, the RSU informs the CA of the new rsu ID. Here, we again use the CA REQ structure with an enabledupdate bit. The CA maintains a database withveh ID andrsu ID information, which effectively maps the vehicle identity to the RSU identity under which it is present. typedef VEHID_STORE byte veh_ID; byte rsu_ID; The CA can check whether a vehicle is registered in any other RSU using the database. If it is already registered, the CA informs the RSU about a possible Sybil attack attempt. In this situation, the RSU updates its local storage with the invalid certificate for the particular vehicle. This will prevent the vehicle from obtaining a valid certificate on a subsequent request. The complete RSU and CA proctypes are detailed in Appendices 3A.2 and 3A.3, respectively. Verification. The verification process ensures that no vehicle has a valid loca- tion certificate from two different RSUs at the same time. Each RSU maintains a copy of the currently active location certificate within its range. We use an observer process to verify this property, by having it scan different RSUs and ensuring that each vehicle has only one valid location certificate. In the specifi- cation below, theassert clause fails if two RSUs have a valid certificate for the same vehicle. active proctype Observer() int i; int j; do :: for (i : 1 .. NO_OF_RSU) atomic for(j:1 .. NO_OF_RSU) if :: (i=j && rsu_pidsi 0 && rsu_pidsj 0) - for(k:1 .. NO_OF_VEH) assert((RSUrsu_pidsi:loc_certk 0 && RSUrsu_pidsj:loc_certk 0)); :: else - skip; fi od Figure 3.8 shows the kind of output produced by SPIN. We briefly explain this output:46  Security and Privacy in Internet of Things (IoTs) 0:CA 1:Observer 2::init: 1 3:RSU 3 4:RSU 5 5:Vehicle 7 6:Vehicle 9 veh_rsu_chan11,4,0,–1,0 11 veh_rsu_chan1?1,4,0,–1,0 veh_rsu_chan21,4,0,–1,1 13 15 veh_rsu_chan2?1,4,0,–1,1 rsu_ca_chan1,1,0,0 17 rsu_ca_chan?1,1,0,0 ca_rsu_chan11,1 23 ca_rsu_chan1?1,1 25 rsu_veh_chan11,1,4 rsu_veh_chan1?1,1,4 27 rsu_ca_chan1,2,0,0 29 rsu_ca_chan?1,2,0,0 ca_rsu_chan21,0 ca_rsu_chan2?1,0 35 rsu_veh_chan21,2,–1 37 39 rsu_veh_chan2?1,2,–1 41 veh_rsu_chan21,4,1,4,2 43 veh_rsu_chan2?1,4,2,4,2 45 veh_rsu_chan11,4,2,–1,3 47 veh_rsu_chan1?1,4,2,–1,3 49 rsu_ca_chan1,1,0,0 rsu_ca_chan?1,1,0,0 ca_rsu_chan11,0 55 ca_rsu_chan1?1,0 57 rsu_veh_chan11,1,–1 59 rsu_veh_chan?1?1,1,–1 Figure 3.8: SPIN sequence diagram. The malicious Vehicle 6 is a Sybil node and tries to impersonate Vehicle 5 but keeps obtaining invalid certificates.Sybil Attack Detection in Vehicular Networks  47  5:Vehicle is a legitimate node with identity 1, and 6:Vehicle is a malicious (Sybil) node that is using the same ID as5:Vehicle.  The input received by veh rsu chan1?1,4,0,-1,0 represents the location certificate requested by 5:Vehicle through RSU 3:RSU. This RSU consults with the CA and assigns a valid certificate through rsu veh chan1?1,1,4.  The Sybil node,6:Vehicle, tries to associate with4:RSU but obtains an invalid certificate from the RSU viarsu veh chan2?1,2,-1).  The Sybil node repeatedly tries to obtain a valid certificate, but does not succeed. 3.5 Conclusion This chapter presents a novel approach to Sybil attack detection in a vehicu- lar network based upon both cryptographic and location verification. Such an approach helps avoid exclusive dependence on a CA, which can be a bottleneck in communication. Our approach leads to a semicentralized architecture wherein RSUs also participate in the detection process. The accuracy of the system is modeled using the Promela specification language and verified using the SPIN model checker. One of the shortcomings of our scheme is that it does not consider the hand off between RSUs. At the point of hand off, the vehicle will fail to produce a valid certificate for vehicle-to-vehicle communication. Also, the Promela model presented in this chapter covers only vehicle-to-infrastructure communication. By incorporating the cryptographic modeling along with the vehicle-to-vehicle communication we obtain a more complete coverage of VANET communica- tion. The SPIN model checker does not have the notion of time as a quantitative measure. This is an important factor in security, and the introduction of time into the SPIN model would produce a more powerful verification method of security protocols. Finally, it may be noted that the Sybil attack is one among many types of attacks on vehicular networks. Our goal is to integrate mitigation techniques for different types of attacks into a single abstract model so as to achieve a more secure and effective vehicular network. 3A Appendices 3A.1 Vehicle proctype proctype Vehicle(byte veh_ID; byte rsu_ID;byte loc) CER_REQ cer_req; CER_RES cer_res;48  Security and Privacy in Internet of Things (IoTs) byte new_rsu_ID; veh_pidsveh_ID=_pid; /Setup inital request/ new_rsu_ID=rsu_ID; cer_req.veh_ID=veh_ID; cer_req.veh_loc=loc; cer_req.loc_cert=-1; //Invalid certificate -1 do ::true- cer_req.time=g_curr_time; veh_rsu_channew_rsu_IDcer_req; //send request to RSU g_curr_time=g_curr_time+1; //update time rsu_veh_channew_rsu_ID?cer_res; cer_req.loc_cert=cer_res.loc_cert; //Get response from RSU cer_req.rsu_ID=cer_res.rsu_ID; //Setup new request new_rsu_ID=(cer_res.rsu_ID%NO_OF_RSU)+1;//Increment RSU_ID od 3A.2 RSU proctype / Input : rsu_ID and location of RSU/ proctype RSU(byte rsu_ID;byte loc) int loc_certNO_OF_VEH+1; int i; for(i:1 .. NO_OF_VEH) loc_certi=-1; rsu_pidsrsu_ID=_pid; CER_REQ cer_req; RSU_REQ rsu_req; CO_RES co_res; CER_RES cer_res; int loc_cert_temp; int loc_cert_old; byte req_rsu; do /Listener for cer_req request from vehicle/ ::veh_rsu_chanrsu_ID?cer_req- if ::cer_req.veh_loc-loc=4 - cer_res.veh_ID=cer_req.veh_ID; //Set location response veh_ID cer_res.rsu_ID=rsu_ID; //Set location response rsu_ID loc_cert_old=cer_req.loc_cert; //Taking location certificate rsu_req.veh_ID=cer_req.veh_ID; rsu_req.rsu_ID=rsu_ID; if /For 1st request(without a valid loc_cert)/ ::loc_cert_old==-1- rsu_req.update=0; //Update 0 means vehicle is not registered in any RSU rsu_ca_chanrsu_req; //send RSU request to CA ca_rsu_chanrsu_ID?co_res; //Get response from CA ::loc_cert_old=0- rsu_req_chancer_req.rsu_IDcer_req,rsu_ID; rsu_res_chanrsu_ID?co_res; ::else-skip;Sybil Attack Detection in Vehicular Networks  49 fi if ::co_res.status==1- // loc_cert_temp=cer_req.time+cer_req.veh_loc; loc_certcer_req.veh_ID=loc_cert_temp; cer_res.loc_cert=loc_cert_temp; ::else-cer_res.loc_cert=-1; ::else - cer_res.loc_cert=-1; fi rsu_veh_chanrsu_IDcer_res; if /if request for loc_cert update initamte CA with new RSU_ID/ ::loc_cert_old=0- rsu_req.update=1; rsu_req.old_rsu_ID=cer_req.rsu_ID; rsu_ca_chanrsu_req; ca_rsu_chanrsu_ID?co_res; if ::co_res.status==0-loc_certco_res.veh_ID=-1; ::else-skip; fi ::else - skip; fi /listener for near by RSU request to check validity of certificate / ::rsu_req_chanrsu_ID?cer_req,req_rsu- co_res.veh_ID=cer_req.veh_ID; if ::loc_certcer_req.veh_ID==cer_req.loc_cert- co_res.status=1; loc_certcer_req.veh_ID=-1; ::else - co_res.status=0; fi rsu_res_chanreq_rsuco_res; od 3A.3 CA proctype active proctype CA() RSU_REQ rsu_req; CO_RES co_res; do /listener for request from RSU/ ::rsu_ca_chan?rsu_req - co_res.status=0; co_res.veh_ID=rsu_req.veh_ID; if ::rsu_req.update==0&&vehid_storersu_req.veh_ID==0- vehid_storersu_req.veh_ID=rsu_req.rsu_ID; co_res.status=1; ::rsu_req.update==1-50  Security and Privacy in Internet of Things (IoTs) if ::rsu_req.old_rsu_ID==vehid_storersu_req.veh_ID- vehid_storersu_req.veh_ID=rsu_req.rsu_ID; co_res.status=1; ::else-co_res.status=0; fi ::else-co_res.status=0; fi ca_rsu_chanrsu_req.rsu_IDco_res; od Bibliography 1 Nitish Balachandran and Sugata Sanyal. A review of techniques to mitigate Sybil attacks. Int. J. Adv. Netw. Applic., 4:1514–1518, 2012. 2 Brijesh Kumar Chaurasia and Shekhar Verma. Infrastructure based authen- tication in VANETs. Int. J. Multimed. Ubiquitous Eng., 6(2):41–54, 2011. 3 Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model Checking, MIT Press, Cambridge, MA 1999. 4 John R. Douceur. The Sybil attack. In Peer-to-Peer Systems, pages 251–260, Vol. 2429 of Lecture Notes in Computer Sciences. Springer, 2002. 5 Gilles Guette and Ciara ´n Bryce. Using TPMS to secure behicular ad-hoc networks (VANETs). In Information Security Theory and Practices. Smart Devices, Convergence and Next Generation Networks, pages 106–116. Springer, 2008. 6 Gerard J. Holzmann. The model checker SPIN. IEEE Trans. Softw. Eng., 23(5):279–295, 1997. ¨ ¨ ¨ 7 Go ¨khan Korkmaz, Eylem Ekici, Fu ¨sun Ozgu ¨ner, and Umit Ozgu ¨ner. Urban multi-hop broadcast protocol for inter-vehicle communication systems. In Proceedings of the 1st ACM International. Workshop on Vehicular Ad-hoc Networks, pages 76–85. ACM, 2004. 8 James Newsome, Elaine Shi, Dawn Song, and Adrian Perrig. The Sybil attack in sensor networks: Analysis & defenses. In Proceedings of the 3rd International Symposium on Information Processing in Sensor Networks, pages 259–268. ACM, 2004. 9 Charalampos Papamanthou, Franco P. Preparata, and Roberto Tamassia. Algorithms for location estimation based on RSSI sampling. In Algorithmic Aspects of Wireless Sensor Networks, pages 72–86. Springer, 2008.Sybil Attack Detection in Vehicular Networks  51 10 Soyoung Park, Baber Aslam, Damla Turgut, and Cliff C. Zou. Defense against Sybil attack in vehicular ad-hoc network based on roadside unit support. In Military Communications Conference, 2009. MILCOM 2009. IEEE, pages 1–7. IEEE, 2009. 11 Bryan Parno and Adrian Perrig. Challenges in securing vehicular networks. In Workshop on Hot Topics in Networks (HotNets-IV), pages 1–6. ACM, 2005. 12 Ali Akbar Pouyan and Mahdiyeh Alimohammadi. Sybil attack detection in vehicular networks. Computer Science and Information Technology, 2(4):197–202, 2014. 13 Prabhakar Ranjan and Kamal Kant Ahirwar. Comparative study of VANET and MANET routing protocols. In Proceedings of the International Con- ference on Advanced Computing and Communication Technologies (ACCT 2011), pages 517–523. 14 Mukul Saini, Kaushal Kumar, and Kumar Vaibhav Bhatnagar. Efficient and feasible methods to detect Sybil attack in VANET. Int. J. Eng., 6(4):431– 440, 2013. 15 Amol Vasudeva and Manu Sood. Sybil attack on lowest ID clustering algo- rithm in the mobile ad-hoc network. Int. J. Netw. Security Applic, 4(5):135, 2012. 16 Ravi M. Yadumurthy, Mohan Sadashivaiah, Ranga Makanaboyina, et al. Reliable MAC broadcast protocol in directional and omni-directional trans- missions for vehicular ad-hoc networks. In Proceedings of the 2nd ACM International Workshop on Vehicular Ad-Hoc Networks, pages 10–19. ACM, 2005. 17 Gongjun Yan, Stephan Olariu, and Michele C Weigle. Providing VANET security through active position detection. Comput. Commun., 31(12): 2883–2897, 2008. 18 Jie Zhang. Trust management for VANETs: Challenges, desired properties and future directions. Int. J. Distrib. Sys. Technol. (IJDST), 3(1):48–62, 2012. 19 Tong Zhou, Romit Roy Choudhury, Peng Ning, and Krishnendu Chakrabarty. Privacy-preserving detection of Sybil attacks in vehicular ad- hoc Networks. In Mobile and Ubiquitous Systems: Networking & Services, 2007. MobiQuitous 2007. Fourth Annual International Conference, pages 1–8. IEEE, 2007.