Warning: fopen(/public/southbridge/dream/web/projects/data/stats.txt) [function.fopen]: 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(): supplied argument is not a valid stream resource in /afs/inf.ed.ac.uk/group/dreamers/websites/dream.inf.ed.ac.uk/web/projects/count.php on line 24
Warning: fclose(): supplied argument is not a valid stream resource in /afs/inf.ed.ac.uk/group/dreamers/websites/dream.inf.ed.ac.uk/web/projects/count.php on line 27 Coral
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:
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 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).
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.
