Links
- The Scyther Tool
- Overview
- Installation
- Exercises
- FAQ
Overview
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. |
|---|---|---|---|---|
| v1.1.3-abstract | Download | Version with abstraction methods by Binh Thanh Nguyen and Christoph Sprenger. | ||
After downloading Scyther, check the installation instructions.
News
- March 2016: Binh Thanh Nguyen and Christoph Sprenger's work on abstraction for security protocols has triggered a new version of Scyther: download here. It is much faster for many case studies, check it out.
- 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:
- Scyther has been used to analyse the IKEv1 and IKEv2 protocol suites and the ISO/IEC 9798 family of authentication protocols.
- The tool has also been used to find new multi-protocol attacks on many existing protocols.
- 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.
- The compromising adversaries version of Scyther has been applied to a large amount of Authenticated Key Exchange (AKE) protocols, such as HMQV, UM, NAXOS, and many other protocols. Details are here and here.
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.