Composition Theorems for CryptoVerif and Application to TLS 1.3
Théorèmes de composition pour CryptoVerif et application à TLS 1.3
Résumé
We present composition theorems for security protocols, to compose a key exchange protocol and a symmetric-key protocol that uses the exchanged key. Our results rely on the computational model of cryptography and are stated in the framework of the tool CryptoVerif. They support key exchange protocols that guarantee injective or non-injective authentication. They also allow random oracles shared between the composed protocols. To our knowledge, they are the first composition theorems for key exchange stated for a computational protocol verification tool, and also the first to allow such flexibility.
As a case study, we apply our composition theorems to a proof of TLS 1.3 Draft-18. This work fills a gap in a previous paper that informally claims
a compositional proof of TLS 1.3, without formally justifying it.
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.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...