being used. Model checking, in this case, identified a specification flaw and a
vulnerability that made the implementation open to a denial-of-service attack.
In Modeling and Analysis of Security Protocols [232] Peter Ryan et al. describe
their use of Failure Divergence Refinement (FDR), a model-checking tool