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.
Type de document :
Communication dans un congrès
2014 ACM SIGSAC Conference on Computer and Communications Security, Nov 2014, Scottsdale, United States. ACM, pp.609-620, 2014, 〈10.1145/2660267.2660276〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01102216
Contributeur : Bruno Blanchet <>
Soumis le : lundi 12 janvier 2015 - 11:57:01
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

Collections

Citation

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. ACM, pp.609-620, 2014, 〈10.1145/2660267.2660276〉. 〈hal-01102216〉

Partager

Métriques

Consultations de la notice

105