Advanced models for the OSPF routing protocol

Courtney Darville; Peter Höfner; Franc Ivankovic; Adam Pam

Advanced models for the OSPF routing protocol

Courtney Darville, Peter Höfner, Franc Ivankovic, Adam Pam

School of Computing

Research output: Contribution to journal › Conference paper › peer-review

2 Citations (Scopus)

20 Downloads (Pure)

Abstract

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.

Original language	English
Pages (from-to)	13-26
Number of pages	14
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	355
Publication status	Published - 21 Mar 2022
Event	5th Workshop on Models for Formal Analysis of Real Systems, MARS 2022 - Munich, Germany Duration: 2 Apr 2022 → 2 Apr 2022

Bibliographical note

Copyright the Author(s). Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

Access to Document

Publisher version (open access)Final published version, 452 KBLicence: CC BY

https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?MARS2022.2Licence: CC BY

Cite this

@article{87424f8af454436bb01af98e39469196,

title = "Advanced models for the OSPF routing protocol",

abstract = "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.",

author = "Courtney Darville and Peter H{\"o}fner and Franc Ivankovic and Adam Pam",

note = "Copyright the Author(s). Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.; 5th Workshop on Models for Formal Analysis of Real Systems, MARS 2022 ; Conference date: 02-04-2022 Through 02-04-2022",

year = "2022",

month = mar,

day = "21",

language = "English",

volume = "355",

pages = "13--26",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

publisher = "Open Publishing Association",

}

TY - JOUR

T1 - Advanced models for the OSPF routing protocol

AU - Darville, Courtney

AU - Höfner, Peter

AU - Ivankovic, Franc

AU - Pam, Adam

N1 - Copyright the Author(s). Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

PY - 2022/3/21

Y1 - 2022/3/21

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

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

UR - https://www.scopus.com/pages/publications/85127923000

M3 - Conference paper

AN - SCOPUS:85127923000

SN - 2075-2180

VL - 355

SP - 13

EP - 26

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

T2 - 5th Workshop on Models for Formal Analysis of Real Systems, MARS 2022

Y2 - 2 April 2022 through 2 April 2022

ER -

Advanced models for the OSPF routing protocol

Abstract

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this