Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate

Résumé : TLS 1.3 est la prochaine version du protocole TLS (Transport Layer Security). Sa conception à partir de zéro est une réaction à la fois à la demande croissante de connexions HTTPS à faible latence et à une série d'attaques récentes de haut niveau sur TLS. L'espoir est qu'un nouveau protocole avec de la cryptographie moderne éviterait d'hériter des problèmes des versions précédentes; le danger est que cela pourrait exposer à de nouveaux types d'attaques ou réintroduire d'anciens défauts corrigés dans les versions précédentes de TLS. Après 18 versions préliminaires, le protocole est presque terminé, et le groupe de travail a appelé les chercheurs à analyser le protocole avant publication. Cet article répond en présentant une analyse globale du protocole TLS 1.3 Draft-18. Nous cherchons à répondre à trois questions qui n'ont pas été entièrement traitées dans les travaux antérieurs sur TLS 1.3: (1) TLS 1.3 empêche-t-il les attaques connues sur TLS 1.2, comme Logjam ou Triple Handshake, même s'il est exécuté en parallèle avec TLS 1.2 ? (2) Peut-on vérifier mécaniquement la sécurité calculatoire de TLS 1.3 sous des hypothèses standard (fortes) sur ses primitives cryptographiques? (3) Comment pouvons-nous étendre les garanties du protocole TLS 1.3 aux détails de ses implémentations? Pour répondre à ces questions, nous proposons une méthodologie pour développer des modèles symboliques et calculatoires vérifiés de TLS 1.3 en même temps qu'une implémentation de référence du protocole. Nous présentons des modèles symboliques dans ProVerif pour différentes versions intermédiaires de TLS 1.3 et nous les évaluons contre une riche classe d'attaques, pour reconstituer à la fois des vulnérabilités connues et des vulnérabilités précédemment non publiées qui ont influencé la conception actuelle du protocole. Nous présentons un modèle calculatoire dans CryptoVerif de TLS 1.3 Draft-18 et prouvons sa sécurité. Nous présentons RefTLS, une implémentation interopérable de TLS 1.0-1.3 et analysons automatiquement le coeur de son protocole en extrayant un modèle ProVerif à partir de son code JavaScript typé.
Type de document :
Rapport
[Research Report] RR-9040, Inria Paris. 2017, pp.51
Liste complète des métadonnées


https://hal.inria.fr/hal-01528752
Contributeur : Bruno Blanchet <>
Soumis le : lundi 29 mai 2017 - 16:06:18
Dernière modification le : jeudi 20 juillet 2017 - 09:26:43

Fichier

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

Identifiants

  • HAL Id : hal-01528752, version 1

Collections

Relations

Citation

Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. [Research Report] RR-9040, Inria Paris. 2017, pp.51. <hal-01528752>

Partager

Métriques

Consultations de
la notice

198

Téléchargements du document

103