Attacking Group Protocols by Refuting Incorrect Inductive Conjectures

G. Steel, Alan Bundy

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Automated tools for finding attacks on flawed security protocols often struggle to deal with protocols for group key agreement. Systems designed for fixed 2 or 3 party protocols may not be able to model a group protocol, or its intended security properties. Frequently, such tools require an abstraction to a group of fixed size to be made before the automated analysis takes place. This can prejudice chances of finding attacks on the protocol. In this paper, we describe Coral, our system for finding security protocol attacks by refuting incorrect inductive conjectures. We have used Coral to model a group key protocol in a general way. By posing inductive conjectures about the trace of messages exchanged, we can investigate novel properties of the protocol, such as tolerance to disruption, and whether it results in agreement on a single key. This has allowed us to find three distinct novel attacks on groups of size two and three.
Original languageEnglish
Pages (from-to)149-176
JournalJournal of Automated Reasoning
Issue number1-2
Publication statusPublished - Jan 2006

Keywords / Materials (for Non-textual outputs)

  • cryptographic security protocols
  • counterexamples
  • superposition


Dive into the research topics of 'Attacking Group Protocols by Refuting Incorrect Inductive Conjectures'. Together they form a unique fingerprint.

Cite this