On modeling and formally verifying secure explicit on-demand ad hoc routing protocols

Ad hoc networks represent a promising communication technology that targets the ensuring of connectivity in special scenarios in which dedicated infrastructure cannot be used. The core of ad hoc networks is represented by the ad hoc routing protocols. These routing protocols raise specific security aspects that need to be taken care of. Many propositions of secure ad hoc routing protocols had been made, but very few actual implementations exist and are used. Through the work presented in this paper we present a less applied research methodology that we believe it can increase the confidence in the security of ad hoc networks: formal verification of the security properties of ad hoc routing protocols. Our target is a particular class of routing protocols: secure explicit on-demand ad hoc routing protocols. By taking as a case study Ariadne protocol, we will show how HLPSL and AVISPA can be used to model and to validate the security properties of this kind of routing protocols. We will show that the novelty of our work is given by the tools that are used, because they increase the automation degree of the verification process.