06/10/2009, 16:15 — 17:15 — Room P4.35, Mathematics Building
Bruno Montalto, ETH Zurich, Switzerland
Deciding Security Against Offline Guessing Attacks under Equational
Theories
Offline guessing (or dictionary) attacks are one of the most common
vulnerabilities of security protocols. Previous formalizations of
offline guessing attacks are essentially extensions of the standard
Dolev-Yao model for security protocol analysis with inference rules
which model the attacker's guessing capability, such as those
proposed by Lowe. However, as pointed out by Vigano et. al., such a
set of rules is specialized to a particular set of cryptographic
primitives and intruder capabilities, and it is difficult to
convince oneself of its completeness. In line with this work, we
propose a symbolic method based on equational theories and provide
a simple yet general definition of offline guessing attack in our
model. We also show that, for a particular but relevant class of
equational theories, the problem of deciding whether an attacker
can mount an offline guessing attack from a set of terms learned
during protocol execution is decidable in polynomial-time,
mimicking a result by Delaune and Jacquemard for Lowe's model.
