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 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
External linksSearch via SFX
Journal / seriesTechnical report
Pages / Article No.
Subjectsecurity, cryptographic protocols, formal methods; unbounded verification; authentication; secrecy
Organisational unit03634 - Basin, David
MoreShow all metadata