Lawrence C. Paulson and Roger M. Needham (with thanks to Valeria de Paiva)
Research associates: Kim Wagner (to 31 March 1997), Katherine Eastaughffe
Funded by the EPSRC (1 Jan 1996 to 30 June 1999). Grant reference GR/K77051. Value £157,244
This project developed the inductive approach to verifying cryptographic protocols. The key paper has been cited over 1100 times.
In distributed computing systems, components of the system (people, computers, services: usually called principals) must satisfy themselves mutually that they are who they say they are. This is the reason for authentication protocols. Formal analysis of these protocols is highly desirable for discovering flaws and omissions.
This proposal concerns the study of authentication logics, a widespread formal method used in the verification of security protocols. We make a case for a deeper theoretical analysis of the method, as well as for implementations of the resulting logics in the generic theorem prover Isabelle. In the course of the work, attention has shifted from authentication logics to new methods based upon operational models and inductive proofs.