An On-the-Fly Model-Checker for Security Protocol Analysis

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 DolevYao 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.

• Type: Conference
• Year: 2003
• Where: ESORICS
• Authors: David A. Basin, Sebastian Mödersheim, Luca Viganò
• Keywords: ESORICS 2003, Infinite State Spaces, On-the-fly Model Checker, Security Privacy, Security Protocols