Soundness Limits of Dolev-Yao Models

Abstract : Automated tools such as model checkers and theorem provers for the analysis of security protocols typically abstract from cryptography by Dolev-Yao models, i.e., they replace real cryptographic operations by term algebras. The soundness of Dolev-Yao models with respect to real cryptographic security definitions has received significant attention in the last years. Until recently, all published results were positive, i.e., they show that various classes of Dolev-Yao models are indeed sound with respect to various soundness definitions. Here we discuss impossibility results. In particular, we present such results for Dolev-Yao models with hash functions, and for the strong security notion of blackbox reactive simulatability (BRSIM)/UC. We show that the impossibility even holds if no secrecy (only collision resistance) is required of the Dolev-Yao model of the hash function, or if probabilistic hashing is used, or certain plausible protocol restrictions are made. We also survey related results for XOR. In addition, we start to make some impossibility results explicit that tacitly underly prior soundness results in the sense of motivating unusual choices in the Dolev-Yao models or the realizations. We also start to discuss which of the problems known for BRSIM/UC soundness extend to weaker soundness notions.
Type de document :
Communication dans un congrès
Véronique Cortier et Steve Kremer. Workshop on Formal and Computational Cryptography (FCC 2006), Jul 2006, Venice/Italy, 2006
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00080678
Contributeur : Véronique Cortier <>
Soumis le : mardi 20 juin 2006 - 15:01:22
Dernière modification le : mardi 31 octobre 2017 - 14:22:18
Document(s) archivé(s) le : lundi 5 avril 2010 - 23:06:55

Fichier

Identifiants

  • HAL Id : inria-00080678, version 1

Collections

Citation

Michael Backes, Birgit Pfitzmann, Michael Waidner. Soundness Limits of Dolev-Yao Models. Véronique Cortier et Steve Kremer. Workshop on Formal and Computational Cryptography (FCC 2006), Jul 2006, Venice/Italy, 2006. 〈inria-00080678〉

Partager

Métriques

Consultations de la notice

135

Téléchargements de fichiers

390