Trustworthy Systems

A mechanized proof of loop freedom of the (untimed) AODV routing protocol

Authors

Timothy Bourke, Robert van Glabbeek and Peter Höfner

INRIA
France

Ecole normale supérieure

NICTA

UNSW

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 paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interac- tive 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 au- tomatically and identify exactly the steps that are no longer valid.

BibTeX Entry

  @inproceedings{Bourke_GH_14_2,
    address          = {Sydney, Australia},
    author           = {Bourke, Timothy and van Glabbeek, Robert and H\"ofner, Peter},
    booktitle        = {International Symposium on Automated Technology for Verification and Analysis (ATVA)},
    doi              = {10.1007/978-3-319-11936-6_5},
    editor           = {{F. Cassez and J.-F. Raskin}},
    month            = nov,
    pages            = {47--63},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8080.pdf},
    publisher        = {Springer},
    title            = {A mechanized proof of loop freedom of the (untimed) {{AODV}} routing protocol},
    year             = {2014}
  }

Download