Edinburgh Research Explorer

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

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

Related Edinburgh Organisations

Documents

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
Pages137-151
Number of pages15
ISBN (Electronic)978-3-540-25984-8
ISBN (Print)978-3-540-22345-0
DOIs
StatePublished - 2004

Publication series

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

Abstract

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.

Download statistics

No data available

ID: 6322582