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