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

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

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

		Timothy Bourke Mechanization of the Algebra for Wireless Networks (AWN) [AWN] Archive of Formal Proofs, 2014
		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

Trustworthy Systems