Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures

G. Steel, Alan Bundy, M. Maidl

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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
Title of host publicationAutomated Reasoning
Subtitle of host publicationSecond International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004. Proceedings
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Electronic)978-3-540-25984-8
ISBN (Print)978-3-540-22345-0
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
ISSN (Print)0302-9743


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

Cite this