Scyther is a tool for the automatic verification of security protocols.
For a performance comparison between Scyther and a number of other tools, please read the comparison paper.

The latest version of Scyther is 1.0-beta7 (with Gutsy Gibbon patch), which was released on 13 December 2007.

Download

Download and install Scyther 1.0-beta7.

Additionally, you may want to look at the Scyther exercise set which is very useful for giving a course on security protocols.

News

  • September 2009: Added instructions to the Frequently Asked Questions list for users of Mac OS 10.6, Snow Leopard.
  • August 2009: A new version of Scyther is almost ready for release. It provides support for many types of compromising adversaries. This version will provide support for perfect forward secrecy, key compromise impersonation, session-key compromise, and adversaries capable of state-reveal queries. To be released soon. (Status: currently being optimized and soon going into testing phase for all three platforms.) For more information, check out this paper.

Features

Scyther is an automated security protocol verification tool. Some interesting features are:

  • Scyther can verify protocols with an unbounded number of sessions and nonces.
  • Scyther can characterize protocols, yielding a finite representation of all possible protocol behaviours.
  • The performance of Scyther is state-of-the-art, as can be read in detail in this comparison of security protocol analysis tools.

  • The semantics of protocol execution, security properties and input language are based on the Operational Semantics for security protocols.
  • It has been used among other things to find new multi-protocol attacks on many existing protocols.
  • The algorithm expands on ideas developed for the Athena tool by X.D. Song (which is currently unavailable). Scyther improves on Athena for a number of reasons:
    • Even when used with a bound on the number of sessions, it can decide (i.e. prove or disprove) a large class of protocols.
    • Multi-protocol analysis is handled in an intuitive way (concatenation of input files.)
    • It can verify ordering-related properties such as synchronisation
    • Multiple key infrastructures (PKIs) can be modeled.
    • Scyther has a graphical user interface and can show attacks as they are found.
  • The tool comes bundled with a set of example protocol files modeled from the SPORE repository, which is set up to be an online continuation of the Clark-Jacob library of authentication protocols.

Papers on Scyther

Please visit my publications page for the details either on the tool paper (CAV 2008), or the algorithm paper (CCS 2008). Additional details can be found in my PhD Thesis.

There are also a number of papers which use Scyther (also by other authors), but they are not listed here (yet).

Isabelle/HOL support

Currently, work is underway to have full support for the underlying protocol model in the Isabelle/HOL theorem proving environment.

The full details on this development, as well as downloadable snapshots of the theory, can be found on the FOSSP pages maintained by Simon Meier.

Mailing list

People using Scyther are recommended to subscribe to the Scyther-users mailing list. If new versions of the tool are released, an announcement will be made on the mailing list.