Attacking the Asokan-Ginzboorg Protocol for Key Distribution in an Ad-Hoc Bluetooth Network Using CORAL
Proceedings of 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems
We describe Coral, a counterexample finder for incorrect inductive conjectures. By devising a first-order version of Paulson's formalism for cryptographic protocol analysis, 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 attacks we have found on the Asokan--Ginzboorg protocol for establishing a group key in an ad-hoc network of Bluetooth devices.