@TechReport{ cremers:scyther:2007, abstract = {We present a new cryptographic protocol verification tool called Scyther. The tool is state-of-the-art in terms of verification speed and provides a number of novel features. (1) It can verify most protocols for an unbounded number of sessions in less than a second. Because no approximation methods are used, all attacks found are actual attacks on the model. (2) In cases where unbounded correctness cannotbe determined, the algorithm functions as a classical bounded verification tool, and yields results for a bounded number of sessions. (3) Scyther can give a ``complete characterization'' of protocol roles, allowing protocol designers to spot unexpected possible behaviours early. (4) Contrary to most other verification tools, the user is not required to provide so-called scenarios for property verification, as all possible protocol behaviours are explored by default. The algorithm expands on ideas from the Athena algorithm. We describe the algorithm, choice of heuristics, and discuss experimental results. The tool has been used already successfully for research as well as teaching of security protocol analysis.}, author = {Cas Cremers}, institution = {ETH Zurich}, language = {USenglish}, month = {Aug}, number = 572, title = {Scyther: Unbounded Verification of Security Protocols}, year = 2007, user = {cremersc} }