Routing Information Protocol in HOL/SPIN

We provide a proof using HOL and SPIN of convergence for the Routing Information Protocol (RIP), an internet protocol based on distance vector routing. We also calculate a sharp realtime bound for this convergence. This extends existing results to deal with the RIP standard itself, which has complexities not accounted for in theorems about abstract versions of the protocol. Our work also provides a case study in the combined use of a higher-order theorem prover and a model checker. er is used to express abstraction properties and inductions, and structure the high-level proof, while the latter deals e ciently with case analysis of nitary properties.

• Type: Conference
• Year: 2000
• Where: TPHOL
• Authors: Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic
• Keywords: Automated Reasoning, Distance Vector Routing, Routing Information Protocol, Sharp Realtime Bound, TPHOL 2000