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.
Gavin Lowe / Oxford University Computing Laboratory, Parks Road, Oxford, OX1
3QD, UK / gavin.lowe@comlab.ox.ac.uk
