Skip to main content

Loop Freedom of AODV in Isabelle/HOL

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

  • Aim: Mechanize an existing pen-and-paper proof of loop freedom of the Ad hoc On-demand Distance Vector (AODV) routing protocol in the interactive theorem prover Isabelle/HOL.
  • Approach: Adapt standard techniques for showing invariants of individual reactive nodes and apply a novel compositional approach for lifting invariants to networks of nodes.
    This combination of techniques works very well and is likely useful for modelling and verifying similar protocols in an interactive theorem prover. We also analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically (once the original proof has been mechanised) and identify exactly the steps that are no longer valid.
  • Collaboration: Inria Paris-Rocquencourt and Ecole normale supérieure (PARKAS team)

People


Publications

2016

Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
Mechanizing a process algebra for network protocols
Journal of Automated Reasoning, Volume 56, Number 3, pp. 309-341, March, 2016

2014

Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
A mechanized proof of loop freedom of the (untimed) AODV routing protocol
International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 47-63, Sydney, Australia, November, 2014
Abstract PDF Timothy Bourke, Rob van Glabbeek and Peter Hoefner
Showing invariance compositionally for a process algebra for network protocols
International Conference on Interactive Theorem Proving, pp. 44-59, Vienna, Austria, July, 2014

Isabelle/HOL Source Code

Proof scripts can be found in the Archive of Formal Proofs (AFP). They are publicly available under the BSD license.
 
Link zu AFP-Entry ISABELLE Timothy Bourke
Mechanization of the Algebra for Wireless Networks (AWN) [AWN]
Archive of Formal Proofs, 2014
Link zu AFP-Entry ISABELLE Timothy Bourke and Peter Höfner
Loop freedom of the (untimed) AODV routing protocol [AODV]
Archive of Formal Proofs, 2014


The proof scripts contain a hierarchy of theory files, whose contents are summarised below. The files are best viewed in the Isabelle proof assistant, which can be downloaded for free and installed under Windows, Mac, or Linux. The files in bold above can then be opened by typing, for example
       isabelle jedit aodv/Aodv_Loop_Freedom.thy
Once Isabelle has processed a .thy file, you can hold down the ctrl key and click on elements of the proof text to see their formal definitions.
 
Generic Files [AWN, AODV]
Lib.thy Generic functions and lemmas
TransitionSystems.thy Transition systems (automata)
Invariants.thy Reachability and Invariance
OInvariants.thy Open reachability and invariance
Algebra of Wireless Networks (AWN) and its Proof Theory [AWN]
awn/Toy.thy Simple toy example
awn/AWN_Main.thy Import all AWN-related theories
awn/AWN.thy Terms of the Algebra for Wireless Networks
awn/AWN_SOS.thy Semantics of the Algebra of Wireless Networks
awn/AWN_Labels.thy Labelling sequential processes
awn/AWN_SOS_Labels.thy Configure the inv_cterms tactic for sequential processes
awn/AWN_Cterms.thy Control terms and well-definedness of sequential processes
awn/Pnet.thy Lemmas for partial networks
awn/Closed.thy Lemmas for closed networks
awn/OAWN_SOS.thy Open semantics of the Algebra of Wireless Networks
awn/OAWN_SOS_Labels.thy Configure the inv_cterms tactic for open sequential processes
awn/OPnet.thy Lemmas for open partial networks
awn/OClosed_Lifting.thy Lifting rules for (open) closed networks
awn/Inv_Cterms.thy A custom tactic for showing invariants via control terms
awn/AWN_Invariants.thy Generic invariants on sequential AWN processes
awn/OAWN_Invariants.thy Generic open invariants on sequential AWN processes
awn/OAWN_Convert.thy Transfer standard invariants into open invariants
awn/Qmsg.thy Model the standard queuing model
awn/Qmsg_Lifting.thy Lifting rules for parallel compositions with QMSG
awn/ONode_Lifting.thy Lifting rules for (open) nodes
awn/OPnet_Lifting.thy Lifting rules for (open) partial networks
awn/OClosed_Transfer.thy Transfer open results onto closed models
AODV Loop Freedom [AODV]
aodv/Aodv_Loop_Freedom.thy Apply invariants to show loop freedom of the AODV model
aodv/Aodv_Basic.thy Constants used in all AODV variants
aodv/Aodv_Data.thy Predicates and functions used in the AODV model
aodv/Aodv_Message.thy Messages used in the AODV protocol
aodv/Aodv.thy Model an instance of the AODV protocol
aodv/Aodv_Predicates.thy Predicates for stating invariant assumptions and properties
aodv/OAodv.thy Adapt the AODV model for the open semantics
aodv/Fresher.thy Relations (of quality) between routes
aodv/Quality_Increases.thy Predicate and lemmas for quality increases
aodv/Seq_Invariants.thy Invariant proofs over individual sequential processes
aodv/Global_Invariants.thy Invariant proofs over open sequential processes
aodv/Loop_Freedom.thy Routing graphs and loop freedom from invariance
AODV Variants [AODV]
aodv_tr_verA/Aodv_Loop_Freedom.thy Loop freedom of AODV variant A
aodv_tr_verB/Aodv_Loop_Freedom.thy Loop freedom of AODV variant B
aodv_tr_verC/Aodv_Loop_Freedom.thy Loop freedom of AODV variant C
aodv_tr_verD/Aodv_Loop_Freedom.thy Loop freedom of AODV variant D
aodv_tr_verE/Aodv_Loop_Freedom.thy Loop freedom of AODV variant E

Contact

Peter Höfner, peter.hoefner <at> data61.csiro.au
Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.