Edinburgh Research Explorer

Attacking Group Protocols by Refuting Incorrect Inductive Conjectures

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions

Open

Documents

Original languageEnglish
Pages (from-to)149-176
JournalJournal of Automated Reasoning
Volume36
Issue number1-2
DOIs
StatePublished - Jan 2006

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.

    Research areas

  • cryptographic security protocols, counterexamples, superposition

Download statistics

No data available

ID: 402065