Formal security analysis of a secure on-demand routing protocol for AD HOC networks using model checking

Abstract

An ad hoc network is a self-configuring network of mobile terminals, connected by wireless links and exhibiting nomadic behavior by freely moving within an area. Computing the routes between the terminals in the ad hoc environment and delivering a guarantee of communication have never been achieved by any protocol in its entirety. In this work, we model an ad hoc network to model-check ARIADNE in order to verify one of its powerful security properties. By a similar approach to Buttyμan’s Active-1-2 attack on ARIADNE, we have used SPIN to flag a sequence of possible events in the protocol leading to a new Active-2-2 attack, where two compromised nodes collaborate to remove all intermediate nodes from the route-discovery process.