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
2 ENS Paris - École normale supérieure - Paris
3 NICTA - National ICT Australia [Sydney]
4 UNSW - University of New South Wales [Sydney]
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.
Keywords : AODV protocol verification Isabelle/HOL
Document type :
Conference papers
Liste complète des métadonnées
https://hal.inria.fr/hal-01092360
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

arxiv

Identifiers

Collections

INRIA | ENS-PARIS | PSL | INRIA-ROCQ

Citation

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〉

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

167

Contact


archive-ouverte@inria.fr