ABSTRACT
It is necessary for practitioners of formal methods to be aware of the array of tools available that support the formal verification of cryptographic protocols. This chapter presents several such automated tools, namely: Maude-NPA, Tamarin, ProVerif, Casper FDR, Scyther, CL-AtSe, OFMC and SATMC. A summary of their capabilities is presented to aid in directly comparing the tools, alongside an overview of the real world protocols to which the tools have been successfully applied, including: TLS, IKE, EMV and Kerberos. The chapter considers the Needham-Schroeder Public Key protocol to illustrate the similarities and differences between the tools, presenting the way in which the protocol, the intruder, and the protocol properties are modeled and analyzed. It intends to support practitioners in determining the correct tool for their context by consistently presenting the input and outputs of the tools and highlighting their similarities, differences and merits.
