I have a long history of getting grant money that I cannot use, because I have moved, or because the partner changed his/her mind, etc.

It started with the project "Authentication Logics", which I mostly wrote for co-P.I's Larry Paulson and Roger M. Needham in 1995. Larry had been my sponsor in the previous project on "Evaluation Logic" with Andrew Pitts and I was really grateful when he accepted the idea of a project on authentication logics and invited Prof. Needham. I was also grateful to Kim Wagner, who stepped in to be the RA, when I was offered a proper lectureship in Birmingham and moved there in January 1996.

Of course they changed completely the direction of the project, which was about theory and implementation in Isabelle and ended up being about a new method in Isabelle, i.e. a totally different, but quite interesting new theory and mostly its implementation.

Larry's project page, linked above, says:

#
Authentication Logics:

It started with the project "Authentication Logics", which I mostly wrote for co-P.I's Larry Paulson and Roger M. Needham in 1995. Larry had been my sponsor in the previous project on "Evaluation Logic" with Andrew Pitts and I was really grateful when he accepted the idea of a project on authentication logics and invited Prof. Needham. I was also grateful to Kim Wagner, who stepped in to be the RA, when I was offered a proper lectureship in Birmingham and moved there in January 1996.

Of course they changed completely the direction of the project, which was about theory and implementation in Isabelle and ended up being about a new method in Isabelle, i.e. a totally different, but quite interesting new theory and mostly its implementation.

Larry's project page, linked above, says:

#
Authentication Logics:

New Theory and Implementations

**Lawrence C. Paulson and Roger M. Needham (with thanks to Valeria de Paiva)**

Research associates: Kim Wagner (to 31 March 1997), Katherine Eastaughffe

*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.