Information Security Seminar 

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.