A mechanized proof of loop freedom of the (untimed) AODV routing protocol
 Aim: Mechanize an existing penandpaper proof of loop freedom of the Ad hoc Ondemand 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 reestablish most proof obligations automatically (once the original proof has been mechanised) and identify exactly the steps that are no longer valid.  Collaboration: Inria ParisRocquencourt 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. 309341, 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. 4763, 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. 4459, 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.thyOnce 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 AWNrelated 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 welldefinedness 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 