We are interested in collaboration on the Logical Verification of Security Protocols, either via applicants for PhD positions or via visitors to the Department of Computer Science at the University of Liverpool.
Work in this area within the Department of Computer Science tackles the representation of protocols within a logical framework and the verification of security properties of such protocols using logic-based tools. This work involves collaboration between members of the Agent ART and Logic & Computation research groups. Specifically:
As more and more information is transferred electronically, and as the sensitivity of this data increases, there is clearly an increasing need to provide mechanisms for ensuring the security of information transfer between computers. In addition, with the advent of grid and ubiquitous computing, security and trust are key issues that are integral to the success of these technologies. This need for security has led to the development of cryptographic protocols, in which authentication of the individuals and messages concerned (typically through encryption) occurs. Given the importance of the area, it is vital that techniques be used which provide automatic analysis of such protocols prior to deployment.
Ever since the security of information transfer between computers became an issue, it has been clear that formal methods should have a key part to play in analysing protocol security. Not surprisingly, a wide range of tools for the formal verification of security aspects have been developed. Typically, these involve either full (or at least abstracted) state-space exploration, for example via model checking, or complex theorem-proving using higher-order tools. While both these types of approach have made significant advances, neither is completely satisfactory: the first has limitations with infinite state spaces (even with abstraction techniques); the second suffers from complexity of the human intervention required, and the lack of heuristics having high probability of success. A more appealing solution lies in between these two, namely to use proof methods, but to restrict the logic to decidable or semi-decidable fragments. While such a restriction is not always possible, there are a wide range of protocols where analysis of this style can be effective. In particular, many authentication techniques that can be captured in terms of the temporal change in the participants' knowledge and belief fall into this category.
Temporal logic is an extension of classical logic that is widely used in the specification and verification of complex systems. In this type of logic, time is an added dimension and so logical properties can evolve over time; consequently this form of logic is very suitable for systems that change over time, such as dynamic or adaptive systems. Temporal logic has been used in many areas within Computer Science and Artificial Intelligence, including the specification and verification of reactive (e.g. distributed or concurrent) systems, the synthesis of programs from temporal specifications, algorithmic verification via model-checking, knowledge representation and reasoning, and temporal databases.
A temporal logic of knowledge or belief is a temporal logic enriched by the addition of modal connectives for representing the knowledge (usually the modal logic S5) or belief (usually the modal logic KD45) of a group of processes. These logics can be used to formalise reasoning such as: ``if process P1 knows that process P2 has received message M1, then P1 should eventually send message M2 to P2''. Temporal logics of knowledge and belief are also widely used in the specification and verification of distributed and multi-agent systems.
This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.70)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -no_navigation -split 1 -no_subdir -address M.Fisher@csc.liv.ac.uk sec_research.tex
The translation was initiated by Michael Fisher on 2006-03-29