Proved Implementations of Cryptographic Protocols in the Computational Model

Résumé : Le but de ce travail est d'obtenir des implémentations de protocoles cryptographiques prouvées dans le modèle calculatoire. Nous avons implémenté un compilateur qui prend une spécification d'un protocole dans le langage d'entrée du vérificateur de protocoles CryptoVerif et compile celle-ci en une implémentation en OCaml. Nous avons prouvé le secret des clés échangées et l'authentification du serveur de l'échange de clés du protocole SSH (Secure SHell), puis nous avons utilisé notre compilateur sur celui-ci. Nous avons prouvé que ce compilateur est correct : si un adversaire est capable de casser une propriété de sécurité dans le code généré avec probabilité p, alors il existe un adversaire capable de casser cette propriété sur la spécification avec la même probabilité p. Si une spécification est prouvée sûre dans le modèle calculatoire par CryptoVerif, alors l'implémentation générée est aussi sûre.
Type de document :
Thèse
Cryptography and Security [cs.CR]. Paris 7, 2013. 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-01112630
Contributeur : Bruno Blanchet <>
Soumis le : mardi 3 février 2015 - 12:36:59
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mercredi 27 mai 2015 - 16:06:08

Fichier

Identifiants

  • HAL Id : tel-01112630, version 1

Collections

Citation

David Cadé. Proved Implementations of Cryptographic Protocols in the Computational Model. Cryptography and Security [cs.CR]. Paris 7, 2013. English. 〈tel-01112630〉

Partager

Métriques

Consultations de la notice

111

Téléchargements de fichiers

151