Verification of cryptographic protocols: techniques and link to cryptanalysis

Véronique Cortier 1
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 (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Security protocols are short programs aiming at securing communications over a network. They are widely used in our everyday life. Their verification using symbolic models has shown its interest for detecting attacks and proving security properties. In particular, several automatic tools have been developed. However, the guarantees that the symbolic approach offers have been quite unclear compared to the computational approach that considers issues of complexity and probability. This later approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. In this talk, we present several techniques used for symbolically verifying security protocols and we show that it is possible to obtain the best of both worlds: fully automated proofs and strong, clear security guarantees. For example, for the case of protocols that use signatures and asymmetric encryption, we establish that symbolic integrity and secrecy proofs are sound with respect to the computational model against an active adversary.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Sixth International Workshop on Automatic Verification of Critical Systems - AVOCS'06, Sep 2006, Nancy/France, 2006
Liste complète des métadonnées

https://hal.inria.fr/inria-00091656
Contributeur : Stephan Merz <>
Soumis le : mercredi 6 septembre 2006 - 18:55:14
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : jeudi 20 septembre 2012 - 10:20:44

Fichier

Identifiants

  • HAL Id : inria-00091656, version 1

Citation

Véronique Cortier. Verification of cryptographic protocols: techniques and link to cryptanalysis. Stephan Merz and Tobias Nipkow. Sixth International Workshop on Automatic Verification of Critical Systems - AVOCS'06, Sep 2006, Nancy/France, 2006. 〈inria-00091656〉

Partager

Métriques

Consultations de la notice

166

Téléchargements de fichiers

79