Proofs: Verification of Routing protocols

Formal verification of standards for distance vector routing protocols

This directory contains the source files for the automatic verification of the distance vector routing protocols: Routing Information Protocol (RIP) [1,2] and Ad-hoc On-demand Distance Vector Routing Protocol (AODV) [3,4]. These proofs are referenced in our papers [5] and [6].

The proofs for RIP are here. The proofs for AODV are here.

The following files contain specific proofs mentioned in the papers:

RIP: Complete HOL proof script is here

RIP: HOL proof for k-stability is here

RIP: HOL proof for abstraction is here

RIP: Spin files to prove that k-stability is preserved by advertisements are here

RIP: Spin files to prove that k-stability results in k+1-stability within two rounds of adverts are here

RIP: Spin files to prove that k+1-stability is preserved by advertisements are here

RIP: Spin files to prove that k+1-stability results in k+2-stability within one round of adverts. here

RIP: PVS theory for RIP is here

RIP: PVS proof script for RIP is here

AODV: SPIN files used for finding counter-examples (looping scenarios) are here

AODV: SPIN files to prove the loop-free invariants are here

AODV: HOL proofs for loop freedom (rely on SPIN results) are here

Bibliography

[1]	C. Hendrick. Routing Information Protocol. IETF RFC 1058, June 1988. TXT
[2]	G. Malkin. RIP Version 2 Carrying Additional Information. IETF RFC 1723, November 1994. TXT
[3]	Charles E. Perkins and Elizabeth M. Royer. Ad-hoc on-demand distance vector routing. In Proceedings of the 2nd IEEE Workshop on Mobile Computer Systems and Applications, pages 90-100, February 1999. PS
[4]	Charles E. Perkins and Elizabeth M. Royer. Ad Hoc On Demand Distance Vector ({AODV}) Routing. IETF Internet Draft Version 2, March 1998. TXT
[5]	Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter. Formal verification of standards for distance vector routing protocols, 2000. Working Paper. Presented in the Recent Research Session at Sigcomm 1999.
[6]	Karthikeyan Bhargavan, Carl A. Gunter, and Davor Obradovic. RIP in SPIN/HOL, Theorem Proving and Higher Order Logics, August 2000. Download PS.