31/01/2012, 16:15 — 17:15 — Room P3.31, Mathematics Building
Bruno Montalto, ETH Zurich
FAST: An efficient decision procedure for Static Equivalence and
Message Deducibility for subterm convergent equational theories
Cryptographic protocols are widely used to provide secure
communication over insecure networks, and much work has been
devoted to ensure their correctness. Symbolic approaches to this
task have achieved significant success: based on them, several
automatic protocol verification tools have been implemented, and
these have been successful in finding many protocol attacks.
Message deducibility and static equivalence are two central
problems in these approaches. The attacker's capabilities are
usually expressed in terms of message deducibility, i.e., which
messages can the attacker learn. Static equivalence is an
indistinguishability-based notion of knowledge that can be used to
model strong secrecy and has has been used, e.g., to study off-line
guessing attacks and e-voting protocols. FAST is an efficient
decision procedure for these two problems under subterm convergent
equational theories. This class of equational theories is
sufficient for describing a broad range of cryptographic
primitives. In this talk we compare FAST with other existing tools,
both in terms of theoretical complexity and performance in
practice. For subterm convergent equational theories, FAST has a
significantly better asymptotic complexity, and its performance in
practice confirms this: for many practically relevant examples,
FAST terminates in under a second, whereas other tools take several
minutes.
