Routing information protocol in hol/spin

Abstract

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. The former is used to express abstraction properties and inductions, and structure the high-level proof, while the latter deals efficiently with case analysis of finitary properties.