An on-the-fly model-checker for security protocol analysis

121Citations
Citations of this article
41Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Cite

CITATION STYLE

APA

Basin, D., Mödersheim, S., & Viganò, L. (2003). An on-the-fly model-checker for security protocol analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2808, pp. 253–270). Springer Verlag. https://doi.org/10.1007/978-3-540-39650-5_15

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free