Cas Cremers

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

We are also actively developing two related tools, scyther-proof and Tamarin, whose relations are summarized in this feature comparison table.

The latest stable version of Scyther is v1.1.3, which was released on April 4, 2014.

Download

Version Linux Windows Mac OS X Comments
v1.1.3 Download Download Download This is the standard version.
Compromise-0.9.2 Download Download Download Choose this if you need support for various adversary models.

After downloading Scyther, check the installation instructions.

News

  • May 2014: Released Scyther versions v1.1.3 and compromise-0.9.2 for Mac OS X.
  • April 2014: Released Scyther versions v1.1.3 and compromise-0.9.2 for Linux and Windows. Mac OS X updates coming soon.
  • December 2013: Released Scyther versions v1.1.2 and compromise-0.9.1 for Linux, Mac OS X, and Windows. An overview of the changes for v1.1.2 is provided in the changelog. The compromising adversaries version contains its own changelog in the base directory.
  • October 2013: Released Scyther versions v1.1.1 and compromise-0.9 for Linux and Windows. Mac OS X updates coming soon.
  • December 2012: Released Scyther versions v1.1 and compromise-0.8.
  • July 2012: Released Scyther versions v1.0 and compromise-0.7.1.
  • April 2012: New versions of Scyther are now available on the download page. They contain various bugfixes and minor improvements. Additonally, they now allow for directly specifying correspondence assertions using Lowe-style 'Running' and 'Commit' claims.
  • March 2011: (Compromising adversaries version) An alternative release of Scyther is available here. It allows for analysis with respect to a class of adversary models and contains a large number of other improvements. The only drawback is that it can be slower on some problems that can also be dealt with be the normal version, which will be addressed in a future release.

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.
  • It is efficient: comparison of security protocol analysis tools.
  • The semantics of protocol execution, security properties, and its underlying algorithm are described in this book.

Protocols analysed with Scyther

Some selected protocols that have been analysed with Scyther:

The above list is far from complete. Many more source files are included in the distribution, or can be directly downloaded here.

We also describe a selection of protocol models for our tools on the protocol models page.

Papers on Scyther

Please visit the publications page for the details either on the tool paper (CAV 2008), or the algorithm paper (CCS 2008). The book is also highly recommended.

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

Contribute

If you would like to contribute protocol models, please contact Cas Cremers.

If you would like to contribute to the development of the Scyther tool, read the below:

Development and source files

Since November 2012, development of Scyther has moved to Github:

Please visit the repository page to download the sources, help with development, or report issues.

Using Scyther in teaching

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

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.