### 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.

### License

BSD License

### Topics

- Computer science/Concurrency/Process calculi

### Session AODV

- Aodv_Basic
- Aodv_Data
- Aodv_Message
- Aodv
- Aodv_Predicates
- Fresher
- Seq_Invariants
- Quality_Increases
- OAodv
- Global_Invariants
- Loop_Freedom
- Aodv_Loop_Freedom
- A_Norreqid
- A_Aodv_Data
- A_Aodv_Message
- A_Aodv
- A_Aodv_Predicates
- A_Fresher
- A_Seq_Invariants
- A_Quality_Increases
- A_OAodv
- A_Global_Invariants
- A_Loop_Freedom
- A_Aodv_Loop_Freedom
- B_Fwdrreps
- B_Aodv_Data
- B_Aodv_Message
- B_Aodv
- B_Aodv_Predicates
- B_Fresher
- B_Seq_Invariants
- B_Quality_Increases
- B_OAodv
- B_Global_Invariants
- B_Loop_Freedom
- B_Aodv_Loop_Freedom
- C_Gtobcast
- C_Aodv_Data
- C_Aodv_Message
- C_Aodv
- C_Aodv_Predicates
- C_Fresher
- C_Seq_Invariants
- C_Quality_Increases
- C_OAodv
- C_Global_Invariants
- C_Loop_Freedom
- C_Aodv_Loop_Freedom
- D_Fwdrreqs
- D_Aodv_Data
- D_Aodv_Message
- D_Aodv
- D_Aodv_Predicates
- D_Fresher
- D_Seq_Invariants
- D_Quality_Increases
- D_OAodv
- D_Global_Invariants
- D_Loop_Freedom
- D_Aodv_Loop_Freedom
- E_All_ABCD
- E_Aodv_Data
- E_Aodv_Message
- E_Aodv
- E_Aodv_Predicates
- E_Fresher
- E_Seq_Invariants
- E_Quality_Increases
- E_OAodv
- E_Global_Invariants
- E_Loop_Freedom
- E_Aodv_Loop_Freedom
- All

### Depends on

- Mechanization of the Algebra for Wireless Networks (AWN)

## Cite

×

AODV-AFP

    @article{AODV-AFP,
      author  = {Timothy Bourke and Peter Höfner},
      title   = {Loop freedom of the (untimed) AODV routing protocol},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/AODV.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Nov 3, 2014 : Isabelle2014
- Nov 1, 2014 : Isabelle2014