Model checking cryptographic protocols subject to combinatorial attack. - Roscoe, T; Nguyen., L (2011)
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.