Loop freedom of the (untimed) AODV routing protocol

Timothy Bourke 1, 2, 3 Peter Höfner 3, 4
2 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : The Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (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 development mechanises an existing pen-and-paper proof of loop freedom of AODV. The protocol is modelled in the Algebra of Wireless Networks (AWN), which is the subject of an earlier paper and AFP mechanization. The proof relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several variants of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.
Type de document :
Autre publication
Entry in the Archive of Formal Proofs (ISSN: 2150-914x). 2014, pp.496
Liste complète des métadonnées

Contributeur : Timothy Bourke <>
Soumis le : jeudi 15 janvier 2015 - 20:38:07
Dernière modification le : mercredi 28 septembre 2016 - 13:54:15
Document(s) archivé(s) le : vendredi 11 septembre 2015 - 06:53:31


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01104033, version 1



Timothy Bourke, Peter Höfner. Loop freedom of the (untimed) AODV routing protocol. Entry in the Archive of Formal Proofs (ISSN: 2150-914x). 2014, pp.496. <hal-01104033>



Consultations de
la notice


Téléchargements du document