Model checking of security protocols has proved very successful at finding flaws. Briefly: a model is built of a small system running the protocol, together with the most general attacker who can interact with that system; a model checker is then used to explore the state space of the protocol, looking for attacks. I will explain the technique, with particular reference to modelling in CSP, and checking using the model checker FDR.
I will consider application-layer protocols that are built on top of a secure transport protocol (such as SSL). I will argue that this two-layer approach makes for a cleaner, simpler design: the secure transport layer can protect against dishonest outsiders, so that the application-layer protocol need only protect against dishonest outsiders. I'll also talk about how such a protocol can be analysed, abstracting away from the details of the transport protocol, and modelling only the services it provides.
This is based on work with Philippa Hopcroft (Broadfoot)