Model Checking Ad Hoc Network Routing Protocols: ARAN vs. endairA

Several different secure routing protocols have been proposed for determining the appropriate paths on which data should be transmitted in ad hoc networks. In this paper, we focus on two of the most relevant such protocols, ARAN and end air A, and present the results of a formal analysis that we have carried out using the AVISPA Tool, an automated model checker for the analysis of security protocols. By model checking ARAN with the AVISPA Tool, we have discovered three attacks (a route disruption, a route diversion, and a creation of incorrect routing state), while our analysis of end air A revealed no attacks.