Automated Symbolic Proofs of Observational Equivalence

Many cryptographic security definitions can be naturally formulated as observational equivalence properties. However, existing automated tools for verifying the observational equivalence of cryptographic protocols are limited: they do not handle protocols with mutable state and an unbounded number of sessions. We propose a novel definition of observational equivalence for multiset rewriting systems. We then extend the Tamarin prover, based on multiset rewriting, to prove the observational equivalence of protocols with mutable state, an unbounded number of sessions, and equational theories such as Diffie-Hellman exponentiation. We demonstrate its effectiveness on case studies, including a stateful TPM protocol. Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Formal methods; K.4.4 [Electronic Commerce]: Security General Terms Security, Verification Keywords Protocol verification, observational equivalence, symbolic model

• Type: Journal
• Year: 2015
• Where: CCS
• Authors: David A. Basin, Jannik Dreier, Ralf Sasse
• Keywords: CCS 2015, Security Privacy