  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.
