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
Type de document :
Communication dans un congrès
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〉
Liste complète des métadonnées
https://hal.inria.fr/hal-01092360
Contributeur : Timothy Bourke <>
Soumis le : lundi 8 décembre 2014 - 15:53:16
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Lien texte intégral

arxiv

Identifiants

Collections

INRIA | ENS-PARIS | PSL

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

140

Contact


archive-ouverte@inria.fr