Security Protocols
Model checking techniques: The CSP/FDR framework
Security protocols are traditionally described in the literature as a series of messages between the various legitimate participants; at a slightly more abstract level, one could regard this as a number of processes in parallel sending and receiving messages between one another, as specified by the protocol description in question. Since CSP is a notation designed specifically for describing systems that are composed of processes in parallel and communicating with one another by synchronisations upon common events (reflecting the sending and receiving of messages), it is ideal for modelling security protocols. Furthermore, using the model checker FDR (developed by Formal Systems Ltd.), we are able to perform any necessary analysis upon the protocol modelled. This method, and model checkers in general, have indeed proved to be extremely effective at finding attacks upon security protocols (examples of attacks captured using the CSP/FDR framework can be found in the publications list).
The application of this framework to the analysis of security protocols was initiated and developed mainly by Gardiner, Goldsmith, Jackson, Lowe and Roscoe.
The book titled Modelling and analysis of security protocols by Michael Goldsmith, Gavin Lowe, Bill Roscoe, Peter Ryan and Steve Schneider, provides a detailed and thorough understanding of this formal framework.
Casper: Compiler for the Analysis of Security Protocols
Model checkers (in our case, FDR) have proved to be extremely effective in checking for, and finding, attacks upon security protocols. However, the process of creating the CSP protocol models is time-consuming, error-prone and requires a substantial knowledge of the CSP language. Casper is a program, developed by Lowe (1998), that takes a more abstract description of a protocol and generates the corresponding CSP description. The CSP output file is such that it can be loaded directly into FDR, and the requested checks upon the protocol automatically tested. The style of the protocol descriptions in a Casper input script is based on that in the literature and is therefore familiar to users who are interested in modelling them.
Casper has been extended over the years to include: standard CSP modelling techniques, data independence techniques, simplifying transformations, algebraic equivalences.
Data independence techniques
Model checkers such as FDR have proved to be a very useful and effective tool for modelling security protocols. In particular, FDR has proved to be very successful in finding attacks on protocols. Unfortunately, FDR does not allow processes to be defined with infinite-ranged parameters. This means that one is restricted to verifying finite instances of security protocol models. In addition to this constraint, the size of these sets must remain relatively small to avoid the state space of the implementation exploding to an unmanageable size. So, whilst this framework is excellent for finding attacks upon protocols, one is unable to draw conclusions to the security of the protocols when an attack has not been found.
Over the last few years, Roscoe and Broadfoot have extended the standard CSP framework for modelling protocols to allow a more complete analysis using the FDR model checker, than hitherto. In particular, we are interested in being able to reason about unbounded sequential agent runs as well as higher (and in some cases arbitrary) degrees of parallelism, still within the confines of a finite model. These models rely upon the application of data independence techniques developed by Roscoe and Lazic, and their natural applicability to security protocols within the CSP framework.
There are a number of papers written on this subject and can be found in our security research group's publication list.
Designing security protocols using a layered approach
We are interested in techniques for designing and analysing distributed security transactions. In a recent paper, we presented a layered approach, with a high-level security transaction layer running on top of a lower-level secure transport protocol. The secure transport protocol provides protection against dishonest outsiders, while the transaction layer can be designed to provide protection against dishonest insiders. We specified generic services that one might expect such secure transport protocols to provide. We gave examples of this layered approach, with the aim of demonstrating that the separation of concerns allows for a cleaner, more intuitive design. We also considered how to analyse such a layered security architecture.
Compositionality of Security Properties and Mechanisms
Analysing security protocols has been a much researched area over the last few years; some successfully proved correct and others found to be flawed. One problem seems to be that this must be done for every new protocol, in case the various building blocks making it up have been composed poorly and allow an attack of some kind.
One of our research aims is to take standard mechanisms or building blocks for security protocols (such as DH Key exchange, RSA cryptography and PKI authentication) and abstract these to their specifications, what they require and what they achieve. Once we have these larger modules (like key exchange, secrecy and authentication) we can build a framework to allow abitrary composition of the modules to give secure protocols which achieve all the goals of the components. Then all we have to do is prove the framework does not introduce attacks once, and allow other people to create mechanisms which fit the module specifications and prove them, and the whole system will then be provably secure.
Security aspects within the EU DataGrid Project
We are currently looking at security aspects within the EU DataGrid project, in collaboration with Rutherford Appleton Laboratory and CERN. Areas of interest include: delegation mechanisms, authorisation issues, scalability.