This website contains supplemental material for the paper
Implementing and Proving the TLS 1.3 Record Layer. K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, J. Pan, J. Protzenko, A. Rastogi, N. Swamy, S. Zanella-Béguelin, J. K. Zinzindohoué. In 38th IEEE Symposium on Security and Privacy, IEEE Computer Society 2017.
The following report includes additional materials and proofs of the results in Sections III-V of the paper:
Implementing and Proving the TLS 1.3 Record Layer, K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, J. Pan, J. Protzenko, A. Rastogi, N. Swamy, S. Zanella-Béguelin, J. K. Zinzindohoué. Cryptology ePrint Archive, Report 2016/1178.
All verified code we report on in the paper can be obtained by cloning the Everest project repository in GitHub.
For convenience we have created a branch called record-layer-tr that contains a snapshot at the time of this writing.
To obtain the code, run
$ git clone https://github.com/project-everest/everest --branch record-layer-tr $ cd everest $ ./everest pull
The specifications, implementations and proofs of the record-layer constructions
are located in the
The code can be built and run using
$ ./everest make
The code encompases several open-source projects, namely:
The F*, including libraries for fixed-size integer arithmetic and buffers.
The KreMLin compiler from F* to C.
The development version of miTLS, extended to TLS 1.3, implemented in F*. While verification of the full codebase is in progress, the repository contains verified protocol-specific code for the record layer fragment reported in the paper.
The HACL* cryptographic library, notably including our verified code for cryptographic algorithms and the AEAD construction.