Verification of Security Protocols with Lists: from Length One to Unbounded Length - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

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

Résumé

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.
Fichier principal
Vignette du fichier
PaiolaBlanchetPOST12LV.pdf (300.83 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00863387 , version 1 (18-09-2013)

Identifiants

  • HAL Id : hal-00863387 , version 1

Citer

Miriam Paiola, Bruno Blanchet. Verification of Security Protocols with Lists: from Length One to Unbounded Length. First Conference on Principles of Security and Trust (POST'12), 2012, Tallinn, Estonia. pp.69--88. ⟨hal-00863387⟩

Collections

INRIA INRIA2
64 Consultations
147 Téléchargements

Partager

Gmail Facebook X LinkedIn More