Implementing TLS with Verified Cryptographic Security

Abstract : TLS is possibly the most used protocol for secure communications, with a 18-year history of flaws and fixes, ranging from its protocol logic to its cryptographic design, and from the Internet standard to its diverse implementations. We develop a verified reference implementation of TLS 1.2. Our code fully supports its wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation, as prescribed in the RFCs; it interoperates with mainstream web browsers and servers. At the same time, our code is carefully structured to enable its modular, automated verification, from its main API down to computational assumptions on its cryptographic algorithms. Our implementation is written in F# and specified in F7. We present security specifications for its main components, such as authenticated stream encryption for the record layer and key establishment for the handshake. We describe their verification using the F7 typechecker. To this end, we equip each cryptographic primitive and construction of TLS with a new typed interface that captures its security properties, and we gradually replace concrete implementations with ideal functionalities. We finally typecheck the protocol state machine, and obtain precise security theorems for TLS, as it is implemented and deployed. We also revisit classic attacks and report a few new ones.
Type de document :
Communication dans un congrès
IEEE Symposium on Security & Privacy, 2013, San Francisco, United States. pp.445-462, 2013
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00863373
Contributeur : Ben Smyth <>
Soumis le : lundi 4 avril 2016 - 14:42:04
Dernière modification le : mardi 17 avril 2018 - 11:32:08
Document(s) archivé(s) le : lundi 14 novembre 2016 - 15:58:52

Fichier

implementing-tls-with-verified...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00863373, version 1

Collections

Citation

Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub. Implementing TLS with Verified Cryptographic Security. IEEE Symposium on Security & Privacy, 2013, San Francisco, United States. pp.445-462, 2013. 〈hal-00863373〉

Partager

Métriques

Consultations de la notice

257

Téléchargements de fichiers

112