Formal proof of AODV protocol

Loop freedom is an important property for distance vector routing protocols, especially for the protocols of ad hoc network because the topologies are dynamic. This paper gives a formal description of the AODV protocol and presents a strictly formal proof of its loop freedom property in Isabelle/HOL. The proved theorem states that no loop will exist in any number of nodes. The result demonstrates the feasibility of completely formal verification of some properties of routing protocols with reasonable effort. © 2009 by Binary Information Press.