Open access
Author
Date
2011Type
- Report
ETH Bibliography
yes
Altmetrics
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. Show more
Permanent link
https://doi.org/10.3929/ethz-a-006809966Publication status
publishedJournal / series
Technical Report / ETH Zurich, Department of Computer ScienceVolume
Publisher
ETH, Department of Computer ScienceSubject
VERIFICATION (SOFTWARE ENGINEERING); Security; DATA SECURITY + DATA PROTECTION (OPERATING SYSTEMS); NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); Secrecy; Unbounded verification; NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); VERIFIKATION (SOFTWARE ENGINEERING); Formal methods; Authentication; Cryptographic protocols; DATENSICHERHEIT + DATENSCHUTZ (BETRIEBSSYSTEME)Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science
Notes
Technical Reports D-INFK.More
Show all metadata
ETH Bibliography
yes
Altmetrics