Warning: fopen(/public/southbridge/dream/web/projects/data/stats.txt): failed to open stream: Permission denied in /afs/inf.ed.ac.uk/group/dreamers/websites/dream.inf.ed.ac.uk/web/projects/count.php on line 16 Warning: fwrite() expects parameter 1 to be resource, boolean given in /afs/inf.ed.ac.uk/group/dreamers/websites/dream.inf.ed.ac.uk/web/projects/count.php on line 24 Warning: fclose() expects parameter 1 to be resource, boolean given in /afs/inf.ed.ac.uk/group/dreamers/websites/dream.inf.ed.ac.uk/web/projects/count.php on line 27 Coral
MRG home page · Research · Publications · Projects · Software · People

The Coral Project

Project Description

Coral is a tool for finding counterexamples to inductive conjectures. We have used Coral to find attacks on faulty security protocols, by finding counterexamples to security conjectures in a first-order version of Paulson's inductive model. By refuting conjectures in an inductive model, we can deal with an infinite system directly and avoid having to make simplifying asumptions to create a small finite instance to check. This can be of particular use when dealing with protocols where an indeterminate number of participants may be involved in a single round, i.e. group protocols. So far, Coral has been used to discover 6 novel attacks on 3 group protocols. We are working on building up a corpus of group protocols and attacks.

Attacks Discovered

Coral has been used to discover new attacks on the Asokan-Ginzboorg protocol for group key agreement in an ad-hoc Bluetooth network.

Coral has also discovered new attacks on Taghdiri and Jackson's improved version of the Tanaka-Sato multicast Key management protocol, and the Iolus multicast management protocol.

Details of all these attacks are in the paper Attacking Group Protocols by Refuting Incorrect Inductive Conjectures, by Graham Steel and Alan Bundy, published in 2005 in the Journal of Automated Reasoning. This is the most up-to-date and comprehensive publication on the work.

Implementation

Coral consists of an adapted version of the SPASS theorem prover, modified to pursue a refutation-complete `proof by consistency' strategy like the one proposed by Comon and Nieuwenhuis. The diagram below illustrates the operation of the system. For more details, see the publications below. You can also download Coral.


Future Work

We have plans to try Coral on some more group protocols. We also intend to apply Coral's counterexample finding strategy to other domains.

People

The following people are assosciated with the CORAL project:

Alan Bundy [A.Bundy@ed.ac.uk]Supervisor 
Graham Steel[G.J.Steel@ed.ac.uk]RA, formerly Ph.D. Student 
Monika Maidl[monika@inf.ed.ac.uk]RA  

Publications

  • Attacking Group Protocols by Refuting Incorrect Inductive Conjectures, Graham Steel and Alan Bundy. In Journal of Automated Reasoning, Special Issue on Automated Reasoning for Security Protocol Analysis, December 2005, Pages 1--28. ©Elsevier
    Note: This paper supercedes previous publications on CORAL, group protocols, etc.
  • Attacking a Group Multicast Key Management Protocol using CORAL, Graham Steel and Alan Bundy. In Proceedings of the ARSPA Workshop at IJCAR 2004. Appeared as ENTCS Vol 125 issue 1, pages 125-144.
  • Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures, Graham Steel and Alan Bundy and Monika Maidl. In Proceedings of IJCAR 2004, Springer LNAI 3097, pages 137-151. ©Springer-Verlag
  • Attacking the Asokan--Ginzboorg Protocol for Key Distribution in an Ad-Hoc Bluetooth Network Using CORAL, Graham Steel and Alan Bundy and Monika Maidl. Published in Proceedings of Forte 2003 (work in progress papers).
  • Using the CORAL system to Discover Attacks on Security Protocols Graham Steel and Alan Bundy and Ewen Denney. Chapter in a Fettschrift for Roger Needham entitled Computer Systems: Theory, Technology and Applications, pages 279-286. Edited by Andrew Herbert and Karen Spärck Jones, and published by Springer-Verlag, in December 2003.
  • Finding Counterexamples to Inductive Conjectures and Discovering Security Protocol Attacks. Graham Steel and Alan Bundy and Ewen Denney. Presented at a joint session of the Verify '02 workshop and the Foundations of Computer Security workshop, part of FloC'02, on July 25th 2002. Pages 81-90.
  • Finding Counterexamples to Inductive Conjectures and Discovering Security Protocol Attacks. Graham Steel and Alan Bundy and Ewen Denney. Published in Volume 1 Number 2 (2002) of the AISB Journal, pages 169--182.
  • Funding

    The Coral project was largely funded by EPSRC Rolling Grant GR/M45030, which ended in June 2003.


    Webpage maintained by Graham Steel