N. J. Alfardan and K. G. Paterson, Lucky thirteen: Breaking the TLS and DTLS record protocols, 2013 IEEE Symposium on Security and Privacy, pp.526-540, 2013.

J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, Verifiable side-channel security of cryptographic implementations: Constant-time MEE-CBC, 23rd International Conference on Fast Software Encryption, pp.163-184, 2016.

C. Badertscher, C. Matt, U. Maurer, P. Rogaway, and B. Tackmann, Augmented secure channels and the goal of the TLS 1.3 record layer, 9th International Conference on Provable Security, pp.85-104, 2015.

G. Barthe, C. Fournet, B. Grégoire, P. Strub, N. Swamy et al., Probabilistic relational verification for cryptographic implementations, 41st Annual ACM Symposium on Principles of Programming Languages, pp.193-206, 2014.
DOI : 10.1145/2535838.2535847
URL : https://hal.archives-ouvertes.fr/hal-00935743

M. Bellare and P. Rogaway, The security of triple encryption and a framework for code-based gameplaying proofs, Advances in Cryptology-EUROCRYPT, pp.409-426, 2006.

, Code-based game-playing proofs and the security of triple encryption, Cryptology ePrint Archive, 2004.

M. Bellare and B. Tackmann, The multi-user security of authenticated encryption: AES-GCM in TLS 1.3, Advances in Cryptology-CRYPTO, pp.247-276, 2016.

M. Bellare, O. Goldreich, and A. Mityagin, The power of verification queries in message authentication and authenticated encryption, IACR Cryptology ePrint Archive, p.309, 2004.

D. J. Bernstein, The Poly1305-AES message-authentication code, 12th International Workshopo on Fast Software Encryption, FSE 2005, pp.32-49, 2005.

, Stronger security bounds for Wegman-Carter-Shoup authenticators, Advances in Cryptology-EUROCRYPT 2005, pp.164-180, 2005.

K. Bhargavan and G. Leurent, On the practical (in-)security of 64-bit block ciphers: Collision attacks on HTTP over TLS and OpenVPN, Cryptology ePrint Archive, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01404208

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing TLS with verified cryptographic security, 2013 IEEE Symposium on Security and Privacy, pp.445-459, 2013.
DOI : 10.1109/sp.2013.37
URL : https://hal.archives-ouvertes.fr/hal-00863373

K. Bhargavan, A. Delignat-lavaud, C. Fournet, A. Pironti, and P. Strub, Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS, 2014 IEEE Symposium on Security and Privacy, pp.98-113, 2014.
DOI : 10.1109/sp.2014.14
URL : https://hal.archives-ouvertes.fr/hal-01102259

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, P. Strub et al., Proving the TLS handshake secure (as it is), Cryptology ePrint Archive, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102231

H. Böck, Wrong results with Poly1305 functions, 2016.

H. Böck, A. Zauner, S. Devlin, J. Somorovsky, and P. Jovanovic, Nonce-disrespecting adversaries: Practical forgery attacks on GCM in TLS, Cryptology ePrint Archive, 2016.

C. Boyd, B. Hale, S. F. Mjølsnes, and D. Stebila, From stateless to stateful: Generic authentication and authenticated encryption constructions with application to TLS, Topics in Cryptology-CTRSA 2016, pp.55-71, 2016.
DOI : 10.1007/978-3-319-29485-8_4
URL : https://ntnuopen.ntnu.no/ntnu-xmlui/bitstream/11250/2483752/1/AuthNotions_master.pdf

C. Cremers, M. Horvat, S. Scott, and T. Van-der-merwe, Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication, 2016 IEEE Symposium on Security and Privacy, pp.470-485, 2016.

A. Datta, A. Derek, J. C. Mitchell, and B. Warinschi, Computationally sound compositional logic for key exchange protocols, 19th IEEE Computer Security Foundations Workshop, pp.321-334, 2006.

B. Dowling, M. Fischlin, F. Günther, and D. Stebila, A cryptographic analysis of the TLS 1.3 handshake protocol candidates, 22nd ACM Conference on Computer and Communications Security, pp.1197-1210, 2015.

, A cryptographic analysis of the TLS 1.3 draft-10 full and pre-shared key handshake protocol, 2016.

T. Duong and J. Rizzo, Here come the ? ninjas, 2011.

M. J. Dworkin, Recommendation for block cipher modes of operation: Galois/Counter mode (GCM) and GMAC, National Institute of Standards & Technology, 2007.

M. Fischlin, F. Günther, G. A. Marson, and K. G. Paterson, Data is a stream: Security of stream-based channels, Advances in Cryptology-CRYPTO 2015, pp.545-564, 2015.

M. Fischlin, F. Günther, B. Schmidt, and B. Warinschi, Key confirmation in key exchange: A formal treatment and implications for TLS 1.3, 2016 IEEE Symposium on Security and Privacy, pp.197-206, 2016.

C. Fournet, M. Kohlweiss, and P. Strub, Modular code-based cryptographic verification, 18th ACM Conference on Computer and Communications Security, pp.341-350, 2011.
DOI : 10.1145/2046707.2046746
URL : https://hal.archives-ouvertes.fr/inria-00614372

F. Giesen, F. Kohlar, and D. Stebila, On the security of TLS renegotiation, 2013 ACM Conference on Computer and Communications Security, pp.387-398, 2013.

P. Gutmann, Encrypt-then-MAC for Transport Layer Security (TLS) and Datagram Transport Layer Security (DTLS), IETF RFC, vol.7366, 2014.

T. Jager, F. Kohlar, S. Schäge, and J. Schwenk, On the security of TLS-DHE in the standard model, Advances in Cryptology-CRYPTO, pp.273-293, 2012.

T. Jager, J. Schwenk, and J. Somorovsky, On the security of TLS 1.3 and QUIC against weaknesses in PKCS#1 v1.5 encryption, 22nd ACM Conference on Computer and Communications Security, pp.1185-1196, 2015.

M. Kohlweiss, U. Maurer, C. Onete, B. Tackmann, and D. Venturi, Progress in Cryptology-INDOCRYPT 2015, pp.85-102, 2015.

H. Krawczyk, LFSR-based hashing and authentication, Advances in Cryptology-CRYPTO 1994, pp.129-139, 1994.
DOI : 10.1007/3-540-48658-5_15
URL : https://link.springer.com/content/pdf/10.1007%2F3-540-48658-5_15.pdf

, The order of encryption and authentication for protecting communications (or: how secure is SSL?), Cryptology ePrint Archive, 2001.

, A unilateral-to-mutual authentication compiler for key exchange (with applications to client authentication in TLS 1.3), 23rd ACM Conference on Computer and Communications Security, 2016.

H. Krawczyk and H. Wee, The OPTLS protocol and TLS 1.3, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01378195

H. Krawczyk, K. G. Paterson, and H. Wee, On the security of the TLS protocol: A systematic analysis, Advances in Cryptology-CRYPTO 2013, pp.429-448, 2013.

A. Luykx and K. G. Paterson, Limits on authenticated encryption use in TLS, 2015.

D. Mcgrew and J. Viega, Flexible and efficient message authentication in hardware and software

D. Mcgrew, An interface and algorithms for authenticated encryption, IETF RFC, vol.5116, 2008.

B. Möller, T. Duong, and K. Kotowicz, This POODLE Bites: Exploiting The SSL 3.0 Fallback, 2014.

Y. Nir and A. Langley, ChaCha20 and Poly1305 for IETF protocols, IETF RFC, vol.7539, 2015.

K. G. Paterson, T. Ristenpart, and T. Shrimpton, Tag size does matter: Attacks and proofs for the TLS record protocol, Advances in Cryptology-ASIACRYPT, pp.372-389, 2011.

J. Rizzo and T. Duong, The CRIME Attack, 2012.

J. Salowey, A. Choudhury, and D. Mcgrew, AES Galois Counter Mode (GCM) cipher suites for TLS, vol.5288, 2008.

P. Sarkar, A trade-off between collision probability and key size in universal hashing using polynomials, Cryptology ePrint Archive, 2009.

V. Shoup, On fast and provably secure message authentication based on universal hashing, Advances in Cryptology-CRYPTO, pp.313-328, 1996.

B. Smyth and A. Pironti, Truncating TLS connections to violate beliefs in web applications, Inria, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102013

J. Somorovsky, Systematic fuzzing and testing of TLS libraries, 23rd ACM Conference on Computer and Communications Security, 2016.

N. Swamy, C. Hritcu, C. Keller, A. Rastogi, A. Delignat-lavaud et al., Dependent types and multimonadic effects in F*, 43nd ACM Symposium on Principles of Programming Languages, pp.256-270, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01265793

R. ?wi?cki, ChaCha20/Poly1305 heap-buffer-overflow, 2016.

P. Swire, J. Hemmings, and A. Kirkland, Online privacy and ISPs: ISP access to consumer data is limited and often less than access by others, Georgia Tech, Tech. Rep, 2016.

D. Wagner and B. Schneier, Analysis of the SSL 3.0 protocol, 2nd USENIX Workshop on Electronic Commerce, pp.29-40, 1996.