Towards Unconditional Soundness: Computationally Complete Symbolic Attacker

Gergei Bana 1 Hubert Comon-Lundh 2
2 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. We neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. We propose in this paper a different approach: everything is possible in the symbolic model, unless it contradicts a computational assumption. In this way, we obtain unconditional soundness almost by construction. And we do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works. We set the basic framework, for arbitrary cryptographic primitives and arbitrary protocols, however for trace security properties only.
Type de document :
Communication dans un congrès
2nd Conference on Principles of Security and Trust (POST 2012), 2012, Unknown, spv, 7215, pp.189-208, 2012, llncs
Liste complète des métadonnées

https://hal.inria.fr/hal-00863380
Contributeur : Ben Smyth <>
Soumis le : mercredi 18 septembre 2013 - 17:37:30
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : hal-00863380, version 1

Collections

Citation

Gergei Bana, Hubert Comon-Lundh. Towards Unconditional Soundness: Computationally Complete Symbolic Attacker. 2nd Conference on Principles of Security and Trust (POST 2012), 2012, Unknown, spv, 7215, pp.189-208, 2012, llncs. 〈hal-00863380〉

Partager

Métriques

Consultations de la notice

102