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

DOI10.1007/978-3-319-11936-6_5MaRDI QIDQ3457779zbMATH OpenOpenAlexFDO

Authors Timothy Bourke, Peter Höfner, Rob van Glabbeek

Publication date 17 December 2015

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1505.05646

Mathematics Subject Classification ID

Network protocols (68M12) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: The Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (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.

Recommendations

• Modelling and verifying the AODV routing protocol
• Probabilistic model checking of AODV
• Formal verification of standards for distance vector routing protocols
• Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols
• A process algebra for wireless mesh networks

Cited in

(5)

• Mechanizing a process algebra for network protocols
• AODV
• Modelling and verifying the AODV routing protocol
• scientific article; zbMATH DE number 1670735 (Why is no real title available?)
• Model checking mobile ad hoc networks

Describes a project that uses

Uses Software

• Isabelle/Circus
• Isabelle/HOL

This page was built for publication: A mechanized proof of loop freedom of the (untimed) AODV routing protocol

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3457779)