Model checking cryptographic protocols subject to combinatorial attack

We introduce an approach to model checking cryptographic protocols that use hashing too weak to resist combinatorial attacks. Typically such hashing is used when an extremely low bandwidth channel, such as a human user, is employed to transmit its output. This leads to two opportunities for attack: deducing a weak value from its properties and discovering alternative ways to produce a given weak value. The first of these proves a natural extension to established protocol modelling approaches, but for the second we require something more novel. We propose an approach based on taking snapshots of the intruder memory.

Joint work with Bill Roscoe and Toby Smyth.