Model-Checking Observations
Very effective at finding flaws, but
No guarantee of correctnes, due to artificial finite bounds
Setup and analysis is quick when done by experts
Automatic translation from simple message-list format to model-checker input is possible [Low98a, Mil97]
“Killer” example: Lowe attack on Needham-Schroeder public-key protocol, using FDR [Low96]