EPSRC logo

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 Laboratory
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
No information has been submitted for this grant.
Potential use in non-academic contexts
No information has been submitted for this grant.
Impacts
No information has been submitted for this grant.
Sectors submitted by the Researcher
No information has been submitted for this grant.
Project URL:  
Further Information:  
Organisation Website: http://www.cam.ac.uk