Kind: Master project
Most existing analysis tools for security protocols verify core message exchanges of protocols. The gap between verified protocol cores and real protocol implementations is uncomfortably large, and so is the gap between verified protocol cores and complete official protocol specifications, which are informal and usually very long. Recently, at least two verification tools have been developed that try to narrow these gaps. One of these is fs2pv: a tool for writing verified reference implementations of cryptographic protocols. This tool is based on the F# programming language, a dialect of OCaml that targets Microsoft's Common Language Runtime. In order to verify protocol implementations written in a subset of F#, the fs2pv tool translates F# sources to input for the ProVerif protocol verifier. Another tool for verifying security protocol implementations is Csur, which analyzes annotated protocol implementations in C. There are also tools that automatically generate protocol implementations from formal protocol models, for instance Spi2Java.
In this project, you should use one or more of these tools to carry out some substantial case studies. For instance, you could use fs2pv to develop a verified reference implementation of the SSH protocol. Furthermore, you should thoroughly evaluate and compare these tools, including a comparison of the analysis and verification techniques that they use. Possibly you will have suggestions how to improve or extend some of these tools, and you may even want to implement such extensions.
Prerequisites: Background in verification of security protocols, e.g., as acquired in the Kerckhoffs class Verification of Security Protocols. Good programming skills.
References:
Last modified:
Apr 11, 2009
Christian Haack