Scyther: Unbounded verification of security protocols
OPEN ACCESS
Loading...
Author / Producer
Date
2011
Publication Type
Report
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
We present a new cryptographic protocol verification tool called Scyther. The tool is stateof- 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 cannot be 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.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
572
Pages / Article No.
Publisher
ETH Zurich, Department of Computer Science
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Security; Cryptographic protocols; Formal methods; Unbounded verification; Authentication; Secrecy
Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science