Composition Theorems for CryptoVerif and Application to TLS 1.3

Résumé : Nous présentons des théorèmes de composition pour les protocoles cryptographiques, pour composer un protocole d'échange de clés et un protocole à clé symétrique qui utilise la clé échangée. Nous résultats reposent sur le modèle calculatoire de la cryptographie et sont formulés dans le cadre de l'outil CryptoVerif. Ils autorisent des protocoles d'échange de clés qui garantissent l'authentification injective ou non-injective. Ils autorisent aussi le partage d'oracles aléatoires entre les protocole composés. À notre connaissance, ils sont les premiers théorèmes de composition pour l'échange de clés formulés pour un outil de vérification de protocole dans le modèle calculatoire, et aussi les premiers à autoriser une telle flexibililté. Comme étude de cas, nous appliquons nos théorèmes de composition à une preuve de TLS 1.3 brouillon 18. Ce travail fournit un élément manquant dans un article précédent qui donne informellement une preuve compositionnelle de TLS 1.3, sans la justifier formellement.
Type de document :
Rapport
[Research Report] RR-9171, Inria Paris. 2018, pp.67
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01764527
Contributeur : Bruno Blanchet <>
Soumis le : jeudi 12 avril 2018 - 10:46:45
Dernière modification le : jeudi 19 avril 2018 - 11:10:24

Fichier

RR-9171.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01764527, version 1

Collections

Citation

Bruno Blanchet. Composition Theorems for CryptoVerif and Application to TLS 1.3. [Research Report] RR-9171, Inria Paris. 2018, pp.67. 〈hal-01764527〉

Partager

Métriques

Consultations de la notice

58

Téléchargements de fichiers

22