Comparing state spaces in automatic security protocol verification
Cas J. F. Cremers, Pascal Lafourcade · Repository for Publications and Research Data (ETH Zurich) · 2011
Many tools exist for automatic security protocol verification, and most of them have their own particular language for specifying pro tocols and properties. Several protocol specification models and security properties have been already formally related to each other. However, there is an important 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 homogeneously as possible for each tool. We analyze the performance of the tools over com parable state spaces. This work enables us to effectively compare these automatic tools, i.e. using the same protocol description and exploring the same state space. We also propose some explanations for our exper imental results, leading to a better understanding of the tools.