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. 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

References in zbMATH (referenced in 17 articles , 1 standard article )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Chen, Chen; Jia, Limin; Xu, Hao; Luo, Cheng; Zhou, Wenchao; Loo, Boon Thau: A program logic for verifying secure routing protocols (2015)
  2. Merro, Massimo; Sibilio, Eleonora: A calculus of trustworthy ad hoc networks (2013)
  3. Fehnker, Ansgar; van Glabbeek, Rob; Höfner, Peter; McIver, Annabelle; Portmann, Marius; Tan, Wee Lum: A process algebra for wireless mesh networks (2012)
  4. Ghassemi, Fatemeh; Fokkink, Wan; Movaghar, Ali: Verification of mobile ad hoc networks: an algebraic approach (2011)
  5. Nanz, Sebastian; Nielson, Flemming; Nielson, Hanne Riis: Static analysis of topology-dependent broadcast networks (2010)
  6. Pura, Mihai-Lica; Patriciu, Victor-Valeriu; Bica, Ion: Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study (2010)
  7. Singh, Anu; Ramakrishnan, C.R.; Smolka, Scott A.: A process calculus for mobile ad hoc networks (2010)
  8. Billington, Jonathan; Yuan, Cong: On modelling and analysing the dynamic MANET on-demand (DYMO) routing protocol (2009)
  9. Hoang, Thai Son; Kuruma, Hironobu; Basin, David; Abrial, Jean-Raymond: Developing topology discovery in Event-B (2009)
  10. Espensen, Kristian L.; Kjeldsen, Mads K.; Kristensen, Lars M.: Modelling and initial validation of the DYMO routing protocol for mobile ad-hoc networks (2008)
  11. Saksena, Mayank; Wibling, Oskar; Jonsson, Bengt: Graph grammar modeling and verification of ad hoc routing protocols (2008)
  12. Hojjat, Hossein; Nakhost, Hootan; Sirjani, Marjan: Formal verification of the IEEE 802.1D spanning tree protocol using extended $R$ebeca. (2006)
  13. Nanz, Sebastian; Hankin, Chris: A framework for security analysis of mobile wireless networks (2006)
  14. Kulkarni, Sandeep S.; Bonakdarpour, Borzoo; Ebnenasir, Ali: Mechanical verification of automatic synthesis of fault-tolerant programs (2005)
  15. Bhargavan, Karthikeyan; Obradovic, Davor; Gunter, Carl A.: Formal verification of standards for distance vector routing protocols (2002)
  16. Cansell, Dominique; Gopalakrishnan, Ganesh; Jones, Mike; Méry, Dominique; Weinzoepflen, Airy: Incremental proof of the producer/consumer property for the PCI protocol (2002)
  17. Bhargavan, Karthikeyan; Gunter, Carl A.; Obradovic, Davor: Routing information protocol in HOL/SPIN (2000)