Advanced Models for the OSPF Routing Protocol

Courtney Darville
(University of New South Wales, Sydney, Australia)
Peter Höfner
(School of Computing, ANU, Canberra, Australia)
Franc Ivankovic
(University of Trento, Trento, Italy)
Adam Pam
(Macquarie University, Sydney, Australia)

We present two formal models for the OSPF routing protocol, designed for the model checker Uppaal. The first one is an optimised model of an existing model that allows to check larger network topologies. The second one is a specialised model for adjacency building, a complex subprocedure of OSPF, which is not part of any existing model and which is known to be vulnerable to cyber attacks. We illustrate how both models can be used to discover vulnerabilities in routing protocols.

In Clemens Dubslaff and Bas Luttik: Proceedings Fifth Workshop on Models for Formal Analysis of Real Systems (MARS 2022), Munich, Germany, 2nd April 2022, Electronic Proceedings in Theoretical Computer Science 355, pp. 13–26.
Published: 21st March 2022.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: