The Scyther-Abstraction tool
What is Scyther-Abstraction and how does it work?
The Scyther-Abstraction tool is an extension of the external pageScyther security protocol verification tool with an abstraction module. Given a protocol models and a desired property, this module automatically computes a stack of successively more abstract models and properties (see Figure below) with the most abstract pair at the top. The tool then repeatedly pops such an abstraction from the stack and tries to verify it.
If the verification succeeds then, by soundness of the abstraction process, we can conclude that the original protocol satisfies its properties. If the verification fails, there is an attack on the abstraction. In this case, the module determines whether the attack is real, that is, can be replayed in the original protocol. If so, this is reported to the user. Otherwise, the attack is spurious and the module pops and analyzes the next (more concrete) abstraction from the stack.
Publications related to Scyther-Abstraction
- Binh Thanh Nguyen and Christoph Sprenger. Sound Security Protocol Transformations. POST 2013.
- Binh Thanh Nguyen and Christoph Sprenger. Abstractions for Security Protocol Verification. POST 2015.
- Binh Thanh Nguyen. Sound Abstractions for Security Protocol Verification. Ph.D. Thesis No. 22674, Department of Computer Science, ETH Zurich, May 2015.
- Binh Thanh Nguyen, Christoph Sprenger, and Cas Cremers. Abstractions for Security Protocol Verification. Submitted to JCS, 2015.
Scyther-Abstraction tool download
- The source code of the tool is accessible from external pagegithub.
Links
Here is a link to the original external pageScyther tool, developed by Cas Cremers.