Skip to Main content Skip to Navigation
Conference papers

A Computationally Complete Symbolic Attacker for Equivalence Properties

Abstract : We consider the problem of computational indistinguishability of protocols. We design a symbolic model, amenable to automated deduction, such that a successful inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. We follow the idea we introduced earlier for reachability properties, axiomatizing what an attacker cannot violate. This results a computationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficulties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reachability properties.
Document type :
Conference papers
Complete list of metadata
Contributor : Bruno Blanchet <>
Submitted on : Monday, January 12, 2015 - 11:57:01 AM
Last modification on : Monday, February 15, 2021 - 10:48:53 AM



Gergei Bana, Hubert Comon-Lundh. A Computationally Complete Symbolic Attacker for Equivalence Properties. 2014 ACM SIGSAC Conference on Computer and Communications Security, Nov 2014, Scottsdale, United States. pp.609-620, ⟨10.1145/2660267.2660276⟩. ⟨hal-01102216⟩



Record views