A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems

Véronique Cortier 1 Steve Kremer 2, 3 Bogdan Warinschi 4
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 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 : Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers have been quite unclear. For more than twenty years the two approaches have coexisted but evolved mostly independently. Recently, significant research efforts attempt to develop paradigms for cryptographic systems analysis that combines the best of both worlds. There are two broad directions that have been followed. {\em Computational soundness} aims to establish sufficient conditions under which results obtained using symbolic models imply security under computational models. The {\em direct approach} aims to apply the principles and the techniques developed in the context of symbolic models directly to computational ones. In this paper we survey existing results along both of these directions. Our goal is to provide a rather complete summary that could act as a quick reference for researchers who want to contribute to the field, want to make use of existing results, or just want to get a better picture of what results already exist.
Type de document :
[Research Report] RR-6912, INRIA. 2009, pp.42
Liste complète des métadonnées

Contributeur : Véronique Cortier <>
Soumis le : mercredi 29 avril 2009 - 12:16:39
Dernière modification le : jeudi 9 février 2017 - 15:47:24
Document(s) archivé(s) le : jeudi 10 juin 2010 - 22:15:11


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00379776, version 1


Véronique Cortier, Steve Kremer, Bogdan Warinschi. A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems. [Research Report] RR-6912, INRIA. 2009, pp.42. <inria-00379776>



Consultations de
la notice


Téléchargements du document