M. Abdalla, P. Fouque, and D. Pointcheval, Password-based authenticated key exchange in the three-party setting, IEE Proceedings - Information Security, vol.153, issue.1, pp.27-39, 2006.
DOI : 10.1049/ip-ifs:20055073
URL : https://hal.archives-ouvertes.fr/hal-00918401

D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green et al., Imperfect Forward Secrecy, Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, CCS '15, pp.5-17, 2015.
DOI : 10.1145/2810103.2813707
URL : https://hal.archives-ouvertes.fr/hal-01184171

M. R. Albrecht and K. G. Paterson, Lucky Microseconds: A Timing Attack on Amazon???s s2n Implementation of TLS, EUROCRYPT, pp.622-643, 2016.
DOI : 10.1007/978-3-662-49890-3_24

N. Alfardan, D. J. Bernstein, K. G. Paterson, B. Poettering, and J. C. Schuldt, On the security of RC4 in TLS, USENIX Security Symposium, pp.305-320, 2013.

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, Fast Software Encryption (FSE), pp.163-184, 2016.
DOI : 10.1007/978-3-319-27239-9_6

M. Avalle, A. Pironti, R. Sisto, and D. Pozza, The Java SPI Framework for Security Protocol Implementation, 2011 Sixth International Conference on Availability, Reliability and Security, pp.746-751, 2011.
DOI : 10.1109/ARES.2011.117
URL : http://porto.polito.it/2460419/1/ares2011_author_postprint.pdf

N. Aviram, S. Schinzel, J. Somorovsky, N. Heninger, M. Dankel et al., DROWN: breaking TLS using SSLv2, USENIX Security Symposium, pp.689-706, 2016.

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A Tutorial, Foundations of Security Analysis and Design VII (FOSAD), pp.146-166, 2014.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01114366

M. Bellare, New proofs for NMAC and HMAC: Security without collision-resistance, Advances in Cryptology (CRYPTO), pp.602-619, 2006.
DOI : 10.1007/11818175_36
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.59

M. Bellare, J. Kilian, and P. Rogaway, The Security of the Cipher Block Chaining Message Authentication Code, Journal of Computer and System Sciences, vol.61, issue.3, pp.362-399, 2000.
DOI : 10.1006/jcss.1999.1694

M. Bellare and C. Namprempre, Authenticated encryption: Relations among notions and analysis of the generic composition paradigm, Advances in Cryptology ? ASIACRYPT'00, pp.531-545, 2000.

M. Bellare and P. Rogaway, The Security of Triple Encryption and a Framework??for??Code-Based??Game-Playing??Proofs, Advances in Cryptology (Eurocrypt), pp.409-426, 2006.
DOI : 10.1007/11761679_25

D. J. Bernstein, Curve25519: New Diffie-Hellman Speed Records, Public Key Cryptography (PKC), pp.207-228, 2006.
DOI : 10.1007/11745853_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.4634

B. Beurdouche, K. Bhargavan, A. Delignat-lavaud, C. Fournet, M. Kohlweiss et al., A messy state of the union, IEEE Symposium on Security & Privacy, p.2015
DOI : 10.1145/3023357
URL : https://hal.archives-ouvertes.fr/hal-01114250

K. Bhargavan, C. Brzuska, C. Fournet, M. Green, M. Kohlweiss et al., Downgrade Resilience in Key-Exchange Protocols, 2016 IEEE Symposium on Security and Privacy (SP), pp.506-525, 2016.
DOI : 10.1109/SP.2016.37
URL : https://hal.archives-ouvertes.fr/hal-01425962

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, A. Delignat-lavaud, and S. Maffeis, Language-based defenses against untrusted browser origins, USENIX Security Symposium, pp.653-670, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00863372

K. Bhargavan, A. Delignat-lavaud, and A. Pironti, Verified Contributive Channel Bindings for Compound Authentication, Proceedings 2015 Network and Distributed System Security Symposium, 2015.
DOI : 10.14722/ndss.2015.23277
URL : https://hal.archives-ouvertes.fr/hal-01114248

K. Bhargavan, C. Fournet, R. Corin, and E. Z?linescu, Verified Cryptographic Implementations for TLS, ACM Transactions on Information and System Security, vol.15, issue.1, pp.1-3, 2012.
DOI : 10.1145/2133375.2133378
URL : https://hal.archives-ouvertes.fr/hal-00863381

K. Bhargavan, C. Fournet, and A. D. Gordon, Modular verification of security protocol code by typing, ACM Symposium on Principles of Programming Languages (POPL), pp.445-456, 2010.
DOI : 10.1145/1706299.1706350
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.185.2349

K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse, Verified interoperable implementations of security protocols, ACM Transactions on Programming Languages and Systems, vol.31, issue.1, p.31, 2008.
DOI : 10.1145/1452044.1452049

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing TLS with Verified Cryptographic Security, 2013 IEEE Symposium on Security and Privacy, p.2013
DOI : 10.1109/SP.2013.37
URL : https://hal.archives-ouvertes.fr/hal-00863373

K. Bhargavan and G. Leurent, On the Practical (In-)Security of 64-bit Block Ciphers, Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security , CCS'16, pp.456-467, 2016.
DOI : 10.1145/2976749.2978423
URL : https://hal.archives-ouvertes.fr/hal-01404208

K. Bhargavan and G. Leurent, Transcript Collision Attacks: Breaking Authentication in TLS, IKE, and SSH, Proceedings 2016 Network and Distributed System Security Symposium, 2016.
DOI : 10.14722/ndss.2016.23418
URL : https://hal.archives-ouvertes.fr/hal-01244855

B. Blanchet, Computationally Sound Mechanized Proofs of Correspondence Assertions, 20th IEEE Computer Security Foundations Symposium (CSF'07), pp.97-111, 2007.
DOI : 10.1109/CSF.2007.16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.126.2523

B. Blanchet, A Computationally Sound Mechanized Prover for Security Protocols, IEEE Transactions on Dependable and Secure Computing, vol.5, issue.4, pp.193-207, 2008.
DOI : 10.1109/TDSC.2007.1005

B. Blanchet, Automatic verification of correspondences for security protocols*, Journal of Computer Security, vol.17, issue.4, pp.363-434, 2009.
DOI : 10.3233/JCS-2009-0339

B. Blanchet, Automatically Verified Mechanized Proof of One-Encryption Key Exchange, 2012 IEEE 25th Computer Security Foundations Symposium, pp.325-339, 2012.
DOI : 10.1109/CSF.2012.8
URL : https://hal.archives-ouvertes.fr/hal-00863386

B. Blanchet, Security Protocol Verification: Symbolic and Computational Models, Principles of Security and Trust (POST), pp.3-29, 2012.
DOI : 10.1007/978-3-642-28641-4_2
URL : https://hal.archives-ouvertes.fr/hal-00863388

B. Blanchet, Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends in Privacy and Security, pp.1-135, 2016.
DOI : 10.1561/3300000004
URL : https://hal.archives-ouvertes.fr/hal-01423760

D. Bleichenbacher, Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS #1, Annual International Cryptology Conference, pp.1-12, 1998.
DOI : 10.1007/BFb0055716
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.8543

M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis et al., A trusted mechanised javascript specification, ACM Symposium on the Principles of Programming Languages (POPL), pp.87-100, 2014.
DOI : 10.1145/2535838.2535876
URL : https://hal.archives-ouvertes.fr/hal-00910135

D. Cadé and B. Blanchet, Proved Generation of Implementations from Computationally Secure Protocol Specifications, Journal of Computer Security, vol.23, issue.3, pp.331-402, 2015.
DOI : 10.1007/978-3-642-36830-1_4

S. Chaki and A. Datta, ASPIER: An Automated Framework for Verifying Security Protocol Implementations, 2009 22nd IEEE Computer Security Foundations Symposium, pp.172-185, 2009.
DOI : 10.1109/CSF.2009.20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.151.293

A. Chaudhuri, Flow, Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security , PLAS'16, pp.430-448, 2005.
DOI : 10.1145/2993600.2996280
URL : https://hal.archives-ouvertes.fr/hal-00443919

V. Cortier, S. Kremer, and B. Warinschi, A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems, Journal of Automated Reasoning, vol.13, issue.1, pp.3-4225, 2011.
DOI : 10.1007/s10817-010-9187-9
URL : https://hal.archives-ouvertes.fr/inria-00379776

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 (SP), pp.470-485, 2016.
DOI : 10.1109/SP.2016.35

I. B. Damgård, A Design Principle for Hash Functions, Advances in Cryptology? CRYPTO'89, pp.416-427, 1989.
DOI : 10.1007/0-387-34805-0_39

T. Dierks and E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.2. IETF RFC 5246, 2008.
DOI : 10.17487/rfc5246

Y. Dodis, T. Ristenpart, J. Steinberger, and S. Tessaro, To Hash or Not to Hash Again? (In)Differentiability Results for $$H^2$$ and HMAC, Advances in Cryptology (Crypto), pp.348-366, 2012.
DOI : 10.1007/978-3-642-32009-5_21

D. Dolev and A. C. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-207, 1983.
DOI : 10.1109/TIT.1983.1056650

B. Dowling, M. Fischlin, F. Günther, and D. Stebila, A Cryptographic Analysis of the TLS 1.3 Handshake Protocol Candidates, Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, CCS '15, pp.1197-1210, 2015.
DOI : 10.1145/2810103.2813653

M. Fischlin and F. Günther, Multi-Stage Key Exchange and the Case of Google's QUIC Protocol, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS '14, pp.1193-1204, 2014.
DOI : 10.1145/2660267.2660308

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 (SP), pp.452-469, 2016.
DOI : 10.1109/SP.2016.34

D. Gillmor, Negotiated finite field Diffie-Hellman ephemeral parameters for Transport Layer Security (TLS), 2016.
DOI : 10.17487/RFC7919

S. Goldwasser, S. Micali, and R. Rivest, A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks, SIAM Journal on Computing, vol.17, issue.2, pp.281-308, 1988.
DOI : 10.1137/0217017
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.8353

M. Hamburg, Ed448-Goldilocks, a new elliptic curve. Cryptology ePrint Archive Available at https://eprint.iacr.org, 2015.

R. Hamilton, J. Iyengar, I. Swett, and A. Wilk, QUIC: A UDP-based multiplexed and secure transport, 2016.

K. E. Hickman, The SSL protocol, IETF Internet Draft, 1995.

T. Jager, F. Kohlar, S. Schäge, and J. Schwenk, On the Security of TLS-DHE in the Standard Model, CRYPTO 2012, pp.273-293, 2012.
DOI : 10.1007/978-3-642-32009-5_17

T. Jager, J. Schwenk, and J. Somorovsky, On the Security of TLS 1.3 and QUIC Against Weaknesses in PKCS#1 v1.5 Encryption, Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, CCS '15, pp.1185-1196, 2015.
DOI : 10.1145/2810103.2813657

N. Kobeissi, K. Bhargavan, and B. Blanchet, Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach, IEEE European Symposium on Security and Privacy, p.2017

H. Krawczyk, Cryptographic Extraction and Key Derivation: The HKDF Scheme, Advances in Cryptology (CRYPTO), pp.631-648, 2010.
DOI : 10.1007/978-3-642-14623-7_34
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.593.5659

H. Krawczyk, A Unilateral-to-Mutual Authentication Compiler for Key Exchange (with Applications to Client Authentication in TLS 1.3), Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security , CCS'16, pp.1438-1450, 2016.
DOI : 10.1145/2976749.2978325

H. Krawczyk, K. G. Paterson, and H. Wee, On the Security of the TLS Protocol: A Systematic Analysis, CRYPTO 2013, pp.429-448, 2013.
DOI : 10.1007/978-3-642-40041-4_24

H. Krawczyk and H. Wee, The OPTLS Protocol and TLS 1.3, 2016 IEEE European Symposium on Security and Privacy (EuroS&P)
DOI : 10.1109/EuroSP.2016.18
URL : https://hal.archives-ouvertes.fr/hal-01378195

R. Küsters, T. Truderung, and J. Graf, A Framework for the Cryptographic Verification of Java-Like Programs, 2012 IEEE 25th Computer Security Foundations Symposium, pp.198-212, 2012.
DOI : 10.1109/CSF.2012.9

A. Langley, M. Hamburg, and S. Turner, Elliptic curves for security. IRTF RFC 7748 https, 2016.
DOI : 10.17487/rfc7748

X. Li, J. Xu, Z. Zhang, D. Feng, and H. Hu, Multiple Handshakes Security of TLS 1.3 Candidates, 2016 IEEE Symposium on Security and Privacy (SP), pp.486-505, 2016.
DOI : 10.1109/SP.2016.36

R. Lychev, S. Jero, A. Boldyreva, and C. Nita-rotaru, How Secure and Quick is QUIC? Provable Security and Performance Analyses, 2015 IEEE Symposium on Security and Privacy, pp.214-231, 2015.
DOI : 10.1109/SP.2015.21

U. Maurer and B. Tackmann, On the soundness of authenticate-then-encrypt, Proceedings of the 17th ACM conference on Computer and communications security, CCS '10, pp.505-515, 2010.
DOI : 10.1145/1866307.1866364

N. Mavrogiannopoulos, F. Vercauteren, V. Velichkov, and B. Preneel, A cross-protocol attack on the TLS protocol, Proceedings of the 2012 ACM conference on Computer and communications security, CCS '12, 2012.
DOI : 10.1145/2382196.2382206

C. Meyer, J. Somorovsky, E. Weiss, J. Schwenk, S. Schinzel et al., Revisiting SSL/TLS implementations: New Bleichenbacher side channels and attacks, 23rd USENIX Security Symposium, pp.733-748, 2014.

B. Möller, T. Duong, and K. Kotowicz, This POODLE bites: exploiting the SSL 3.0 fallback, 2014.

N. Fips, 186-3: Digital Signature Standard (DSS) Available at http://csrc.nist. gov/publications/fips, pp.186-189, 2009.

T. Okamoto and D. Pointcheval, The Gap-Problems: A New Class of Problems for the Security of Cryptographic Schemes, Practice and Theory in Public Key Cryptography (PKC), pp.104-118, 2001.
DOI : 10.1007/3-540-44586-2_8

K. G. Paterson, T. Ristenpart, and T. Shrimpton, Tag size does matter: Attacks and proofs for the TLS record protocol Paterson and T. van der Merwe. Reactive and proactive standardisation of TLS, ASIACRYPT Security Standardisation Research (SSR), pp.372-389, 2011.
DOI : 10.1007/978-3-642-25385-0_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.7536

M. Ray, A. Pironti, A. Langley, K. Bhargavan, and A. Delignat-lavaud, Transport Layer Security (TLS) session hash and extended master secret extension, pp.2015-7627

E. Rescorla, 0-RTT and Anti-Replay. https, 2015.

E. Rescorla, [TLS] PR#875: Additional Derive-Secret stage, 2017.

E. Rescorla, M. Ray, S. Dispensa, and N. Oskov, TLS renegotiation indication extension, IETF RFC, vol.5746, 2010.
DOI : 10.17487/rfc5746
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.374.4985

B. Schmidt, S. Meier, C. Cremers, and D. Basin, Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties, 2012 IEEE 25th Computer Security Foundations Symposium, pp.78-94, 2012.
DOI : 10.1109/CSF.2012.25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.377.8368

V. Shoup, Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive, 2004.

D. Stefan, Espectro project description, 2016.

N. Swamy, C. Hri?cu, C. Keller, A. Rastogi, A. Delignat-lavaud et al., Dependent types and multi-monadic effects in F*, ACM Symposium on Principles of Programming Languages (POPL), pp.256-270, 2016.
DOI : 10.1145/2914770.2837655
URL : https://hal.archives-ouvertes.fr/hal-01265793

M. Vanhoef and F. Piessens, All your biases belong to us: Breaking RC4 in WPA-TKIP and TLS, USENIX Security Symposium, pp.97-112, 2015.

D. Wagner and B. Schneier, Analysis of the SSL 3.0 protocol, USENIX Electronic Commerce, 1996.

T. Y. Woo and S. S. Lam, A semantic model for authentication protocols, Proceedings 1993 IEEE Computer Society Symposium on Research in Security and Privacy, pp.178-194, 1993.
DOI : 10.1109/RISP.1993.287633
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.9636

J. K. Zinzindohoue, E. Bartzia, and K. Bhargavan, A Verified Extensible Library of Elliptic Curves, 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp.296-309, 2016.
DOI : 10.1109/CSF.2016.28
URL : https://hal.archives-ouvertes.fr/hal-01425957