Funded DCSL Research Projects       





A New Automated Logic Theory with Attack Detection Capability for the Formal Analysis of Security Protocols
Members:T. Coffey, R. Dojen, A. Jurcut, J. Chen
Sponsor:SFI
Award:Research Frontiers Programme 2011, 11/RFP.1/CMS/3340
Description:This research project proposes the development of a novel logic-based formal verification technique that achieves both objectives of formal security protocol verification: the new technique will simultaneously prove that a security protocol meets its security goals and that it is free of mountable attacks. The proposed technique will have the following key features:
  • Fundamentally different approach to verification, as compared to current logics.
  • Unique attack detection capability, that guarantees to detect the most common forms of attacks: parallel session and replay attacks. Simultaneously, protocols will be formally proven to meet their security goals.
  • The soundness of the new logic will be formally proven.
  • Automated implementation, which removes many potential error sources present in manual verification. The employed automation framework will ensure low resource requirements.

The result of this proposed research will add a completely new dimension to verification logics. It will enable verification logics to “catch up” on ground lost to brute force methods of state-space exploration in security protocol fault detection. It is envisaged, that this research will stimulate further advances in logic-based verification.

In summary, the outcomes of this research will facilitate the development of effective and correct security protocols, which is particularly important in today’s ever-changing communication environment. The outcomes will also lead to improved productivity and reduced time-to-marked for secure online services.


Unified Verification for Security Protocol Design
Members:T. Coffey, R. Dojen, R. Gyorodi, C. Muntean, I. Lasc, A. Luncan
Sponsor:SFI
Award:Research Frontiers Programme 2007, CMSF631
Description:

Formal verification is an imperative, yet highly complex, step in the development of security protocols. This proposal addresses the development of a novel approach to formally determine the trustworthiness of security protocols. While most current verification techniques for security protocols are either based on state-space model checking or modal logics, an innovative unified framework is proposed that joins the abilities of both techniques. In short, modal logics prove that a security protocol meets its design criteria, while state-space-based techniques perform a search for potential attacks. This framework will enable the protocol designer to determine whether a protocol meets its design criteria and prove the absence of potential attacks from a single protocol specification. Thus, it will be able to identify weaknesses revealed by logic-based techniques and state-space-based model checking. Effectively, this is hybridising logical techniques and state-space model checkers. Further this work will reduce the complexity of the formal verification process and an improved readability of the verification results.

The outcomes of this research will increase confidence in the effectiveness and correctness of newly designed security protocols through a novel verification technique that detects weaknesses revealed by logic-based techniques and state-space-based model checking. Further, reduction of the complexity of the development process for security protocols will lead to improved productivity and reduced time-to-marked for online services by enabling security protocol designers to specify and automatically verify the correctness of protocols without in-depth knowledge of the underlying verification techniques.


Automated Verification of Security Protocols
Members:T. Coffey, R. Dojen, T. Newe, I. Salomie
Sponsor:Irish Research Council for Science, Engineering and Technolgoy (IRCSET)
Award:Basic Research Award SC02/237
Description:

This project is aimed at developing an automated cryptographic protocol verification technique based on a logic of knowledge and belief. By using a logic that includes knowledge axioms security issues can be addressed. This is a significant improvement over existing verification technique which use logics of belief and hence can only validate the trust in a protocol.

The chosen logic is that of Coffey and Saidha. The axioms of this logic are sufficiently low-level to express fundamental properties of cryptographic protocols. They also reflect the underlying assumptions of the logic which include the following:

  1. The communication environment is hostile as defined by Bieber
  2. The underlying cryptosystem is ideal.
  3. Keys are considered valid if they have not exceeded their validity period and are only known to the rightful owners.
  4. If a piece of data is encrypted/decrypted, then the entity which performed the encryption/decryption must know the data.
The inference rules of the logic are the standard inference rules of natural deduction. This supports the use of a well-established automated reasoning system as the backbone for the automation of the proving process.

The novel aspects of the proposed work comprises extending the Coffey-Saidha logic to enable it to model hybrid (combined symmetric and public-key) protocols. This requires that the language of the logic is extended and that appropriate axioms to analyse hybrid protocols are added. The extended logic will be able to verify wide range of cryptographic protocols, while existing techniques are directed mainly at authentication and key-agreement protocols. In addition, a proving engine will be used to automate the new technique, thus removing the necessity of protocol designers to fully understand the underlying principles of the proving process.

A further novel aspect of our approach is the use of a logic of knowledge and belief. Thus information concerning protocol security can be obtained. This fundamentally differs from existing techniques which use logics of belief only. Our tool will be unique in its ability to deal also with dishonest principals. These features will be highly valuable to the protocol designer in the development of new cryptographic protocols. The proposed technique, which will provide the ability to reason about knowledge and belief in a protocol is particular important in today's communication environment, where there is an ever-growing demand for security protocols for a variety of applications.