I introduce the on-the-fly model-checker OFMC, a state-of-the-art tool for analyzing security protocols. For example, OFMC can find attacks in a test-suite consisting of 36 well-known flawed protocols in less than a minute of total CPU time. To our knowledge, there is no other tool for finding attacks that is this fast and has comparable coverage. I will also report on a new attack on the Yahalom protocol found by our tool. OFMC owes its success to the combination of two ideas. The first is the modeling of protocols using lazy data-types in a higher-order functional programming language, which allows for the automated analysis of security properties using infinite-state model checking, where the model is explicitly built, on-the-fly, in a demand-driven fashion. The second is the integration of several search optimizations that significantly reduce the infinite search tree associated with a protocol without excluding any attacks. OFMC was developed in the context of the AVISS project, which developed a tool for security protocol analysis that supports the integration of back-ends implementing different search techniques, allowing for their systematic and quantitative comparison and paving the way to their effective interaction.