Formal Analysis of Security Protocols

Many security protocols have appeared in the academic literature, with various goals, such as establishing a cryptographic key, or achieving authentication (where an agent becomes sure of the identity of the other agent taking part in the protocol). These protocols are supposed to succeed even in the presence of a malicious agent, called an intruder; this intruder is assumed to have complete control over the communications network, and so can intercept messages, and introduce new messages into the system using information from messages he has previously seen. Unfortunately, a large proportion of the protocols that have been suggested do not succeed in their stated goals!

The Security Protocol Research Group at Oxford University Computing Laboratory uses the process algebra CSP for the specification, analysis and verification of security protocols.

Our approach is based around the CSP model checker FDR. A small system running the protocol is modelled as a CSP process; the most general intruder who can interact with the protocol is also modelled as a CSP process. FDR is then used to test whether the resulting system satisfies various properties such as "ensures secrecy" or "achieves authentication". If it does not, FDR returns a trace of the system that causes the desired property to fail: this trace corresponds to an attack upon the protocol.

This approach has been applied to several protocols, and has produced a number of attacks.

In order to aid this analysis, we have developed a program Casper that generates the CSP description of the system from a more abstract specification.

It is often not clear precisely what an security protocol is intended to do; in particular, different researchers seem to mean different things by the word authentication. we have identified several different forms of authentication, and formalized them using CSP.

One weakness with the CSP/FDR approach is that it can only be applied to finite (typically small) instances of the protocol. This means that if no attack is found, there may still be an attack upon a larger instance. We are currently investigating under what circumstances it is enough to analyze only small instances: more precisely, we have discovered sufficient conditions under which if there is no attack on a particular small system, then there is no attack upon any larger system.

Many commercial protocols are rather large and complicated. This makes their direct analysis using CSP and FDR infeasible, because of the resulting explosion in the state space and message space sizes; it also makes any other form of analysis more difficult, because of the mass of details. We are therefore investigating safe simplifying transformations for protocols, that is transformations on protocols such that if there is an attack on the original protocol, then there is also an attack on the transformed protocol. The idea is, starting from a large, complicated protocol, to apply as many such transformations as possible, without introducing new attacks; if the resulting protocol is secure, then so is the original.