Skip to Main content Skip to Navigation
Reports

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é.
Complete list of metadatas

Cited literature [85 references]  Display  Hide  Download

https://hal.inria.fr/hal-01528752
Contributor : Bruno Blanchet <>
Submitted on : Thursday, December 20, 2018 - 4:13:41 PM
Last modification on : Thursday, February 7, 2019 - 5:09:35 PM
Document(s) archivé(s) le : Friday, March 22, 2019 - 1:04:01 PM

File

RR-9040.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01528752, version 3

Collections

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-01528752v3⟩

Share

Metrics

Record views

948

Files downloads

524