Improvements to the Security Protocol compiler Casper
Posted: 19th October 2009
Security protocols are short exchanges of messages over a potentially insecure network, with security-related goals, such as establishing a cryptographic key, ensuring the participants are who the claim they are, or carrying out financial transactions. These security protocols are notoriously difficult to get right: many have been suggested, only to later be found to be flawed. Casper is a tool for the analysis of such protocols: it takes a short description of the protocol and compiles it into a model in the process algebra CSP, suitable for analysis using the model checker FDR. During the summer, Tom Gibson-Robinson carried out a project to implement a number of enhancements to Casper. The project was funded under the EPSRC Vacation Bursary scheme, and supervised by Gavin Lowe.
The improvements to Casper included:
- Strengthening the CSP models so as to provide stronger guarantees. Earlier versions of Casper allowed the user to test the protocol only when run by specific systems of agents. The new version (building on ideas by Eldar Kleiner and an earlier implementation by Tilo Buschmann) allows the user to verify the protocol when run on arbitrary systems. In particular, the new version of Casper automates many aspects of the construction of the model, corresponding to theorems in Kleiner's thesis.
- Providing more general techniques for specifying the requirements of protocols. Earlier versions provided a rather limited menu of specification forms, covering just standard security properties. The new version also allows the specifications to be captured using a past-time temporal logic.
- Improved support for analysis of protocols that use timestamps.
- Support for protocols that repeat a sub-protocol an unbounded number of times.
- General improvements to the code and manual, an improved library of example protocols, and an automated testing suite.
