Model checking ARAN ad hoc secure routing protocol with algebraic Petri nets

Modeling and verifying the security protocols for ad hoc networks is a very complex task, because this type of networks is very complex. In this paper we present a new approach: the use of algebraic Petri nets as implemented by AlPiNA tool to model ad hoc networks and to verify some of the security properties of ARAN ad hoc secure routing protocol. The results we have obtained are in concordance with the other research on this protocol, and thus they validate the use of this methodology. Our approach has several advantages. An increase of performance was obtained, in the sense that we managed to verify the protocol for larger topologies than it was previous reported. The specification language of algebraic Petri nets is more expressive than the languages use by other tools, and it is more suited for model based code generation.