Univiversity of Cambridge

Ritter, de Paiva and Ghani have constructed a calculus for explicit substitutions and have together with Alberti constructed a prototype for a linear abstract machine.

An important part of our programme concerns security of protocols. At Cambridge, a new approach to modelling them has been developed, based upon our familiar technique of inductive definitions.

http://www.cl.cam.ac.uk/ftp/papers/reports/ TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.ps.gz

Several versions of the Otway-Rees, Needham-Schroeder and Yahalom protocols have been mechanically analysed using the theorem prover Isabelle. Typically we can show that secrect and authenticity of critical message items even in a partially compromised system. One protocol, designed for an industrial application, was found to be faulty but could be verified after correction.

http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz

Model-checking has been applied to this application, but only under extreme assumptions required to make the state-space finite.

During Larry Paulson's visit to INRIA (Paris) he discussed methods for proving the correctness of cryptographic protocols (using Isabelle) with Valerie Menissier-Morain and Dominique Bolignano, who are pursuing similar investigations (using Coq). For details, see

http://www.cl.cam.ac.uk/users/lcp/papers/protocols