Abstract:


Comparing State Spaces in Automatic Security Protocol Verification


Cas Cremers and Pascal Lafourcade



Many tools exist for automatic security protocol verification, 
and mostof them have their own particular language for specifying 
protocols andproperties. Several protocol specification models 
and securityproperties have been already formally related to each 
other. However,there is an important difference between 
verification tools, which hasnot been investigated in depth before: 
the explored state space. Sometools explore all possible behaviors, 
whereas others explore strictsubsets, often by using so-called 
scenarios. Ignoring such differencescan lead to wrong interpretations 
of the output of a tool. We relate theexplored state spaces to 
each other and find previously unreporteddifferences between the 
various approaches.We apply our study of state space relations in 
a performance comparisonof several well-known automatic tools for 
security protocolverification. We model a set of protocols and their 
properties ashomogeneously as possible for each tool. We analyze the 
performance ofthe tools over comparable state spaces. This work 
enables us toeffectively compare these automatic tools, i.e. using 
the same protocoldescription and exploring the same state space. 
We also propose someexplanations for our experimental results, 
leading to a betterunderstanding of the tools.