Attacking Group Protocols by Refuting Incorrect Inductive Conjectures

Automated tools for finding attacks on flawed security protocols often fail to quately with group protocols. This is because the abstractions made to improve performance on fixed 2 or 3 party protocols either preclude the modelling of group protocols all together, or permit modelling only in a fixed scenario, which can prevent attacks from being discovered. This paper describes Coral, a tool for finding counterexamples to incorrect inductive conjectures, which we have used to model protocols for both group key agreement and group key management, without any restrictions on the scenario. We will show how we used Coral to discover 6 previously unknown attacks on 3 group protocols.

• Type: Journal
• Year: 2006
• Where: JAR
• Authors: Graham Steel, Alan Bundy
• Keywords: Group Protocols, JAR 2006, Party Protocols, Security Protocols