Automatic Verification of Protocols with Lists of Unbounded Length

Abstract : We present a novel automatic technique for proving secrecy and authentication properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions. This result is achieved by extending the Horn clause approach of the automatic protocol verifier ProVerif. We extend the Horn clauses to be able to represent lists of unbounded length. We adapt the resolution algorithm to handle the new class of Horn clauses, and prove the soundness of this new algorithm. We have implemented our algorithm and successfully tested it on several protocol examples, including XML protocols coming from web services.
Type de document :
Communication dans un congrès
CCS'13 - ACM Conference on Computer and Communications Security, Nov 2013, Berlin, Germany. ACM, pp.573--584, 2013, 〈10.1145/2508859.2516679〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00918849
Contributeur : Ben Smyth <>
Soumis le : dimanche 15 décembre 2013 - 17:05:48
Dernière modification le : jeudi 23 novembre 2017 - 01:12:04

Identifiants

Collections

Citation

Bruno Blanchet, Miriam Paiola. Automatic Verification of Protocols with Lists of Unbounded Length. CCS'13 - ACM Conference on Computer and Communications Security, Nov 2013, Berlin, Germany. ACM, pp.573--584, 2013, 〈10.1145/2508859.2516679〉. 〈hal-00918849〉

Partager

Métriques

Consultations de la notice

75