[ Last changed: 19th October 1995 ]

Security Group Seminar, 17th October 1995


Speaker:
Peter Ryan, Defence Research Agency, Malvern

Date:
Tuesday 17th October

Place:
Room TP4, Computer Laboratory

Title:
A CSP APPROACH TO VERIFYING CRYPTOGRAPHIC PROTOCOLS

We give an overview of a research project aimed at applying formal methods to the analysis and design of cryptographic protocols, and present some results on the specification using CSP of their security properties, including authentication, key exchange/distribution, robustness, non-repudiation, integrity, confidentiality and anonymity.

We can also model communications systems, and hostile agents, in CSP, and so we can analyse whether the security properties are upheld. We describe how the CSP model-checker FDR can be used to assist, and illustrate this with examples of how our techniques found flaws in published protocols, and how they can assist in the design of new or improved protocols.


Security Group Seminar, 17th October 1995 / Mark.Lomas@cl.cam.ac.uk