Verification of Security Protocols with Lists: from Length One to Unbounded Length

Abstract : We present a novel, simple technique for proving secrecy properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions. More specifically, our technique relies on the Horn clause approach used in the automatic verifier ProVerif: we show that if a protocol is proven secure by our technique with lists of length one, then it is secure for lists of unbounded length. Interestingly, this theorem relies on approximations made by our verification technique: in general, secrecy for lists of length one does not imply secrecy for lists of unbounded length. Our result can be used in particular to prove secrecy properties for group protocols with an unbounded number of participants and for some XML protocols (web services) with ProVerif.
Type de document :
Communication dans un congrès
Pierpaolo Degano and Joshua Guttman. First Conference on Principles of Security and Trust (POST'12), 2012, Tallinn, Estonia. spv, 7215, pp.69--88, 2012, lncs
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00863387
Contributeur : Ben Smyth <>
Soumis le : mercredi 18 septembre 2013 - 17:37:50
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : vendredi 20 décembre 2013 - 15:02:18

Fichier

PaiolaBlanchetPOST12LV.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00863387, version 1

Collections

Citation

Miriam Paiola, Bruno Blanchet. Verification of Security Protocols with Lists: from Length One to Unbounded Length. Pierpaolo Degano and Joshua Guttman. First Conference on Principles of Security and Trust (POST'12), 2012, Tallinn, Estonia. spv, 7215, pp.69--88, 2012, lncs. 〈hal-00863387〉

Partager

Métriques

Consultations de la notice

92

Téléchargements de fichiers

95