A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol

Timothy Bourke 1, 2 Robert J. Van Glabbeek 3, 4 Peter Höfner 3, 4
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : The (AODV) routing protocol allows the nodes in a (MANET) or a (WMN) to know where to forward data packets. Such a protocol is ‘loop free’ if it never leads to routing decisions that forward packets in circles. This paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.
Liste complète des métadonnées

Contributor : Timothy Bourke <>
Submitted on : Monday, December 8, 2014 - 3:53:16 PM
Last modification on : Wednesday, January 30, 2019 - 11:07:56 AM

Links full text




Timothy Bourke, Robert J. Van Glabbeek, Peter Höfner. A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol. ATVA 2014: Automated Technology for Verification and Analysis, Nov 2014, Sydney, Australia. Springer, Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, 8837, pp.17, 2014, Lecture Notes in Computer Science. 〈http://atva-conferences.org/〉. 〈10.1007/978-3-319-11936-6_5〉. 〈hal-01092360〉



Record views