Analysis of Security Protocols
|
Supervisor |
|
|
Suitable for |
MSc in Computer Science
|
Abstract
A security protocol consists of an exchange of messages between two or more agents, with goals such as establishing a cryptographic key, or authenticating the identities of the agents. These protocols are designed to operate in particularly hostile environments, where an adversary or intruder may be trying to attack the protocol, for example to learn the value of a key. Designing secure protocols has proven to be remarkably difficult; in some cases, attacks have been discovered several years after the protocol was first suggested. We have developed a systematic technique for analysing these protocols. Briefly the technique is as follows:
- The protocol is described formally in an abstract language.
- A compiler called Casper is used to compile the protocol description into a description in the process algebra CSP.
- The CSP description is fed to the model checker FDR, which tests whether the protocol correctly achieves its goals. In the case where the system does not meet a goal, FDR returns a sequence of messages that demonstrates how the goal fails, which is equivalent to the sequence of steps the intruder must take in order to attack the protocol.
A recent extension of these ideas has been to the analysis of layered protocols, where a special-purpose, application-specific
protocol is layered
on top of a general-purpose secure transport layer protocol, such as SSL/TLS.
For such layered
architectures, the CSP model created by Casper abstracts away from the details of the secure transport protocol, and just
models the
security services it provides to the application protocol [3]. The goal of this project would
be to apply this technique to study one or more layered
protocols. An alternative would be to apply these techniques
to so-called human-mediated protocols [4], where a human is responsible for transferring or
verifying some messages
in the protocol; we believe that similar analysis techniques can be applied to such protocols.
Prerequisites:
The Concurrency and Computer Security courses would be prerequisites for this project.
References
- [1] Gavin Lowe, Casper: A Compiler for the Analysis of Security Protocols, Journal of Computer Security, 1998.
- [2] Peter Ryan, Steve Schneider, Michael Goldsmith, Gavin Lowe, Bill Roscoe, Modelling and Analysis of Security Protocols, Addison Wesley, 2001.
- [3] Specifying Secure Transport Layers, Christopher Dilloway, Gavin Lowe. In 21st IEEE Computer Security Foundations
Symposium (CSF 21) 2008.
http://web.comlab.ox.ac.uk//files/116/channels.pdf. - [4] Exploiting Empirical Engagement in Authentication Protocol Design, Sadie Creese, Michael Goldsmith, Richard Harrison,
Bill Roscoe, Paul Whittaker, and
Irfan Zakiuddin. In Proceedings of SPPC 2005, ttp://web.comlab.ox.ac.uk/people/Bill.Roscoe/publications/103.pdf