In Vehicular Ad hoc NETworks (VANETs), vehicles exchange safety messages containing valuable information about traffic environment to increase roads’ safety. The critical nature of these messages entails securing them before considering them. In this context, the credibility and the accuracy assessment of these included safety information arises as a necessity since the consumption of false or imprecise ones by vehicles may cause hazardous consequences. To treat this requirement, we proposed the scheme [1] enabling vehicles to evaluate the credibility and the accuracy of the contents of the safety messages exchanged in VANETs. That scheme is based on three modules: a reputation module, a time and location closeness estimation module, and a majority module. A vehicle can use these modules in a separated or joint way according to the circumstances. Since that scheme is error prone, we conducted in [2], a formal validation, using inference system, to prove the soundness and the completeness of these three modules and their combination. In this paper, we complete that formal validation of [1] by handling the junctions of the three basic modules two by two. To do this, we first completed the inference system in [2] so that the junctions of the three modules two by two become incorporated. A formal verification using this holistic inference system was proposed in a second step to prove the soundness and the completeness of these junctions. This verification's obtained results confirmed the validity of the said junctions for being sound and complete.

In Vehicular Ad hoc NETworks (VANETs), vehicles exchange safety related messages in order to improve the driving experience. However, it is not realistic to presume the absence of attackers intending to subvert the proper operation of the network. While message authentication enables the receiver to make sure of the received message's integrity and to verify its originator, it does not permit the verification of the message's credibility and accuracy. The main contribution of this paper is then the proposition of a scheme to assess the credibility and the accuracy of safety related messages exchanged in VANETs. Three modules constitute our proposal: a reputation module to evaluate the respective reputations of vehicles, a time and location closeness estimation module to judge the accuracy of a reported event and a majority module to decide the trueness of a received traffic information. These modules can be used in a separated or a combined way enabling a more flexibility in front of different circumstances confronted in VANETs. An in-depth security analysis is performed to demonstrate the efficiency of our proposal. Case studies that illustrate the different modules are also presented.