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.
- 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.
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
The semantics of protocol execution, security properties, and its underlying algorithm are described in
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
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
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.
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.