Abstract:

An On-The-Fly Model-Checker for Security Protocol Analysis.

David Basin and Sebastian Mödersheim and Luca Viganò


We introduce 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 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 (but one) known 
attacks and discovers a new one in a test-suite of 36 protocols from the Clark/Jacob library in under one minute 
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.