Experimental Comparison of Automatic Tools for the Formal Analysis of Cryptographic Protocols

The tools for cryptographic protocols analysis based on state exploration are designed to be completely automatic and should carry out their job with a limited amount of computing and storage resources, even when run by users having a limited amount of expertise in the field. This paper compares four tools of this kind to highlight their features and ability to detect bugs under the same experimental conditions. To this purpose, the ability of each tool to detect known flaws in a uniform set of well-known cryptographic protocols has been checked.