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 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.
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.
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.
We have plans to try Coral on some more group protocols. We also intend to apply Coral's counterexample finding strategy to other domains.
The following people are assosciated with the CORAL project:
|Graham Steel||[G.J.Steel@ed.ac.uk]||RA, formerly Ph.D. Student|