Research on Logical Verification of Security in the Department of Computer Science

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.

Sample Publications

  1. N. Agray, W. van der Hoek, and E. de Vink. On BAN Logics for Industrial Security Protocols. In B. Dunin-Keplicz and E. Nawarecki, editors, From Theory to Practice in Multi-Agent Systems. Lecture Notes in Artificial Intelligence vol. 2296, pages 29-36. Springer, 2002.

  2. R. Bordini, M. Fisher, W. Visser, and M. Wooldridge. Model Checking Rational Agents. IEEE Intelligent Systems 19(5):46-52, September/October 2004.

  3. C. Dixon, M.-C. Fernández Gago, M. Fisher and W. van der Hoek. Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols. In Proc. of TIME 2004 -- the 11th International Symposium on Temporal Representation and Reasoning, France, July 2004. IEEE Computer Society Press.

  4. D. Jones. Security Attack Patterns, MSc Dissertation, Department of Computer Science, University of Liverpool, 2005.

  5. M. Fisher, A. Lisitsa, and B. konev. Practical Infinite-state Verification with Temporal Reasoning. In Proceedings of the NATO Advance Reasearch Workshop on Verification of Infinite-State Systems with Applications to Security (VISSAS), 2005.

  6. P. Ballarini, M. Fisher, and M. Wooldridge. Uncertain Agent Verification through Probabilistic Model-Checking. To appear in Proceedings of 3rd International Workshop on Safety and Security in Multiagent Systems (SASEMAS '06)


We also collaborate, on related topics, with:


Department of Computer Science, University of Liverpool, Liverpool L69, United Kingdom.

About this document ...

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 sec_research.tex

The translation was initiated by Michael Fisher on 2006-03-29