Loop Freedom in AODVv2
02 June 2015
The AODV protocol is used to establish routes in a mobile, ad-hoc network (MANET). The protocol must operate in an adversarial environment where network connections and nodes can be added or removed at any point. While the ability to establish routes is best-effort under these conditions, the protocol is required to ensure that no routing loops are ever formed. We present a formal proof of this property for the current form of this protocol, AODVv2, which is currently under consideration at the IETF. Our attempt to construct a formal proof for an earlier version of AODVv2 resulted in the discovery of counter-examples to loop-freedom, and a simple resolution which has been incorporated into the latest version.
