Verification of cryptographic protocols with lists of unbounded lengths

Résumé : Dans cette thèse, nous proposons deux techniques différentes pour la vérification de protocoles de sécurité qui utilisent des listes de taille arbitraire. Dans la première partie de la thèse, nous présentons une technique simple pour vérifier le secret pour des protocoles qui traitent tous les éléments des listes de façon uniforme, pour un nombre non borné de sessions. Plus précisément, cette technique est fondée sur l’approche à base de clauses de Horn utilisée par le vérificateur automatique ProVerif. Nous montrons que si un protocole est prouvé sûr par notre technique avec des listes de longueur un, alors il est sûr pour des listes de longueur arbitraire. Curieusement, ce théorème repose sur des approximations faites par notre technique de vérification : en général, le secret pour des listes de longueur un n’implique pas le secret pour des listes de taille arbitraire. La deuxième technique présentée dans cette thèse permet de prouver automatiquement des propriétés de secret et d’authentification pour des protocoles qui traitent des éléments différents de façon différente. Ce résultat est obtenu en étendant l’approche par clauses de Horn utilisée par ProVerif. Nous étendons la syntaxe des clauses de Horn pour représenter des listes de taille arbitraire. Nous adaptons l’algorithme de résolution pour qu’il traite la nouvelle classe de clauses de Horn et nous prouvons la correction de cet algorithme. Nous avons implémenté notre algorithme et nous l’avons testé avec succès sur plusieurs protocoles, en particulier sur des protocoles pour les services web. Finalement, nous présentons une extension du langage d’entrée de ProVerif, une variante du pi calcul appliqué, pour modéliser les protocoles avec des listes de longueur non bornée, nous en donnons la sémantique et une traduction automatique en clauses de Horn.
Type de document :
Thèse
Cryptography and Security [cs.CR]. Université Paris-Diderot (Paris 7), 2014. English
Liste complète des métadonnées

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

https://hal.inria.fr/tel-01103104
Contributeur : Bruno Blanchet <>
Soumis le : lundi 19 janvier 2015 - 11:27:56
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : vendredi 11 septembre 2015 - 07:07:33

Identifiants

  • HAL Id : tel-01103104, version 2

Collections

Citation

Miriam Paiola. Verification of cryptographic protocols with lists of unbounded lengths. Cryptography and Security [cs.CR]. Université Paris-Diderot (Paris 7), 2014. English. 〈tel-01103104v2〉

Partager

Métriques

Consultations de la notice

255

Téléchargements de fichiers

201