8th European Symposium on Research in Computer Security (ESORICS 2003)
An On-the-Fly Model-Checker for Security Protocol Analysis
David Basin, Sebastian Mödersheim, Luca Viganò
Keywords :
Abstract : We introduce the on-the-fly model-checker OFMC, a tool that combines two methods for analyzing security protocols. The first is the use of lazy data-types as a simple way of building an efficient on-the-fly model checker for protocols with infinite state spaces. The second is the integration of symbolic techniques for modeling a Dolev-Yao intruder, whose actions are generated in a demand-driven way. We present experiments that demonstrate that our tool is state-of-the-art, both in terms of coverage and performance, and that it scales well to industrial-strength protocols.
(Pages 253-270)