Details of Grant 

EPSRC Reference:	GR/K77051/01
Title:	AUTHENTICATION LOGICS: NEW THEORY AND IMPLEMENTATIONS
Principal Investigator:	Paulson, Professor LC
Other Investigators:	Needham, Professor R Needham, Professor R
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science and Technology
Organisation:	University of Cambridge
Scheme:	Standard Research (Pre-FEC)
Starts:	01 January 1996	Ends:	30 June 1999	Value (£):	168,063
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Related Grants:
Panel History:
Summary on Grant Application Form
In distributed computer systems, the various components must convince each other that they are who they say they are. This is the reason for authentication protocols, typically based on cryptography. Formal analysis of these protocols can discover potential security breaches.One of the most successful approaches to the formal analysis of protocols was started by Burrows, Abadi and Needham, who introduced authentication logics. But other authors have criticised such logics, questioning their practical utility and even their correctness. The limitations of such logics have frequently been misunderstood.To rectify this situation requires a deeper analysis of their logical properties. We propose to carry such an analysis using established theoretical tools, both proof-theoretic (for example, natural deduction formalizations) and semantic (for example, modal algebras and categories). The existing semantics of authentication logics is too close to mechanics of authentication protocols. An independent semantics will give the logics greater creditability, and also provide ways of broadening their scope.We expect to develop new, soundly based authentication logics. We also propose to mechanise them using an interactive theorem prover, Isabelle, and to demonstrate them using examples taken from the literature.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.cam.ac.uk