Quelhas T., Sobrinho J.L.

Proceedings of the 10th IASTED International Conference on Parallel and Distributed Computing and Networks, PDCN 2011

pp 139



We present a rigorous correctness proof, formalizable in temporal logic, for the distance vector with reset on failures protocol—an abstraction for a class of shortest-path routing protocols based on diffusing computations. This class includes the diffusing updates algorithm (DUAL), which is at the core of the Enhanced Interior Gateway Routing Protocol (EIGRP), widely used on the Internet. Our rigorous approach allows us to uncover counter-intuitive protocol behaviors which have not been reported previously. We also show that the protocol exhibits exponential message complexity under asynchronous operation, and discuss its applicability beyond shortest-path routing, in particular using the composite bandwidth-delay metric of EIGRP.