Abstract:

OFMC: A Symbolic Model-Checker for Security Protocols

David Basin and Sebastian Mödersheim and Luca Viganò


We present the on-the-fly model-checker OFMC, a tool that combines two ideas for analyzing security protocols 
based on lazy, demand-driven search. The first is the use of lazy data-types as a simple way of building efficient 
on-the-fly model-checkers for protocols with very large, or even infinite, state-spaces. The second is the 
integration of symbolic techniques and optimizations for modeling a lazy Dolev-Yao intruder, whose actions are 
generated in a demand-driven way. We present both techniques, along with optimizations and proofs of 
correctness and completeness. Our tool is state-of-the-art both in terms of coverage and performance. For 
example, it finds all known attacks and discovers a new one in a test-suite of 38 protocols from the Clark/Jacob 
library in a few seconds of CPU time for the entire suite. We also give examples demonstrating how our tool 
scales to, and finds errors in, large industrial-strength protocols.