The proof of AODV loop freedom
Ming Kai Zhou, Huabing Yang, Xingyuan Zhang, Jinshuang Wang · 2009
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.