A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol

Timothy Bourke; Rob van Glabbeek; Peter Höfner; Franck Cassez; Jean-François Raskin

doi:10.1007/978-3-319-11936-6_5

A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol

Timothy Bourke, Rob van Glabbeek, Peter Höfner, Franck Cassez (Editor), Jean-François Raskin (Editor)

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The (AODV) routing protocol allows the nodes in a (MANET) or a (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 paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings
Editors	Franck Cassez, Jean-François Raskin
Publisher	Springer
Pages	47-63
Number of pages	17
ISBN (Electronic)	978-3-319-11936-6
ISBN (Print)	978-3-319-11935-9
DOIs	https://doi.org/10.1007/978-3-319-11936-6_5
Publication status	Published - 24 Oct 2014
Event	12th International Symposium on Automated Technology for Verification and Analysis, 2014 - sYDNEY, Australia Duration: 3 Nov 2014 → 7 Nov 2014 Conference number: 12

Symposium

Symposium	12th International Symposium on Automated Technology for Verification and Analysis, 2014
Abbreviated title	ATVA 2014
Country/Territory	Australia
City	sYDNEY
Period	3/11/14 → 7/11/14

Access to Document

10.1007/978-3-319-11936-6_5Licence: All Rights Reserved

https://link.springer.com/chapter/10.1007/978-3-319-11936-6_5Licence: All Rights Reserved

Cite this

Bourke, T., van Glabbeek, R., Höfner, P., Cassez, F. (Ed.), & Raskin, J.-F. (Ed.) (2014). A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol. In F. Cassez, & J.-F. Raskin (Eds.), Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings (pp. 47-63). Springer. https://doi.org/10.1007/978-3-319-11936-6_5

@inproceedings{05b0d013dbd945f28bb4eaaf930e6499,

title = "A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol",

abstract = "The (AODV) routing protocol allows the nodes in a (MANET) or a (WMN) to know where to forward data packets. Such a protocol is {\textquoteleft}loop free{\textquoteright} if it never leads to routing decisions that forward packets in circles. This paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.",

author = "Timothy Bourke and {van Glabbeek}, Rob and Peter H{\"o}fner and Franck Cassez and Jean-Fran{\c c}ois Raskin",

year = "2014",

month = oct,

day = "24",

doi = "10.1007/978-3-319-11936-6_5",

language = "English",

isbn = "978-3-319-11935-9",

pages = "47--63",

editor = "Cassez, {Franck } and Jean-Fran{\c c}ois Raskin",

booktitle = "Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings",

publisher = "Springer",

address = "United Kingdom",

note = "12th International Symposium on Automated Technology for Verification and Analysis, 2014, ATVA 2014 ; Conference date: 03-11-2014 Through 07-11-2014",

}

Bourke, T, van Glabbeek, R, Höfner, P, Cassez, F (ed.) & Raskin, J-F (ed.) 2014, A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol. in F Cassez & J-F Raskin (eds), Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings. Springer, pp. 47-63, 12th International Symposium on Automated Technology for Verification and Analysis, 2014, sYDNEY, Australia, 3/11/14. https://doi.org/10.1007/978-3-319-11936-6_5

A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol. / Bourke, Timothy; van Glabbeek, Rob; Höfner, Peter et al.
Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings. ed. / Franck Cassez; Jean-François Raskin. Springer, 2014. p. 47-63.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol

AU - Bourke, Timothy

AU - van Glabbeek, Rob

AU - Höfner, Peter

A2 - Cassez, Franck

A2 - Raskin, Jean-François

A2 - Cassez, Franck

A2 - Raskin, Jean-François

N1 - Conference code: 12

PY - 2014/10/24

Y1 - 2014/10/24

N2 - The (AODV) routing protocol allows the nodes in a (MANET) or a (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 paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.

AB - The (AODV) routing protocol allows the nodes in a (MANET) or a (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 paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.

U2 - 10.1007/978-3-319-11936-6_5

DO - 10.1007/978-3-319-11936-6_5

M3 - Conference contribution

SN - 978-3-319-11935-9

SP - 47

EP - 63

BT - Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings

PB - Springer

T2 - 12th International Symposium on Automated Technology for Verification and Analysis, 2014

Y2 - 3 November 2014 through 7 November 2014

ER -

Bourke T, van Glabbeek R, Höfner P, Cassez F, (ed.), Raskin JF, (ed.). A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol. In Cassez F, Raskin JF, editors, Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings. Springer. 2014. p. 47-63 doi: 10.1007/978-3-319-11936-6_5

A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol

Abstract

Symposium

Access to Document

Fingerprint

Cite this