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
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.
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
The following people are assosciated with the CORAL project:
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