@inproceedings{CLN09a,
title = {Comparing State Spaces in Automatic Protocol Analysis },
author = {Cremers, Cas J. F. and Lafourcade, Pascal and Nadeau, Philippe},
year = {2009},
booktitle = {Formal to Practical Security},
pages = {70-94},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
volume = {5458/2009},
team = {DCS},
abstract = {Many tools exist for automatic security protocol verification, and most of them have their own particular language for specifying protocols and properties. Several protocol specification models and security properties have been already formally related to each other. However, there is a further difference between verification tools, which has not been investigated in depth before: the~explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios. Ignoring such differences can lead to wrong interpretations of the output of a tool. We~relate the explored state spaces to each other and find previously unreported differences between the various approaches. We~apply our study of state space relations in a performance comparison of several well-known automatic tools for security protocol verification. We~model a set of protocols and their properties as homogeneous as possible for each tool. We~analyze the performance of the tools over comparable state spaces. This work allows us for the first time to compare these automatic tools fairly, i.e.,~using the same protocol description and exploring the same state space. We~also propose some explanations for our experimental results, leading to a better understanding of the tools.},
}
