Attacking the Asokan-Ginzboorg Protocol for Key Distribution in an Ad-Hoc Bluetooth Network Using CORAL
Graham Steel, Monika Maidl, Alan Bundy · ERA · 2003
Abstract. We describe CORAL, a counterexample finder for incorrect inductive conjectures. By devising a first-order version of Paulson’s formalism for cryptographic protocol analysis, [10], we are able to use CORAL to attack protocols which may have an unbounded number of principals involved in a single run. We show two new attacks CORAL has found on the Asokan–Ginzboorg protocol for establishing a group key in an ad-hoc network of Bluetooth devices, [1].