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

G. Lowe, An attack on the Needham-Schroeder public-key authentication protocol, Information processing letters, vol.56, issue.3, 1995.

M. Roger, M. Needham, and . Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978.

K. Bhargavan, A. Delignat-lavaud, and A. Pironti, Verified contributive channel bindings for compound authentication, Network and Distributed System Security Symposium (NDSS '15), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01114248

C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. Van-der-merwe, A comprehensive symbolic analysis of TLS 1.3, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS '17, pp.1773-1788, 2017.

D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green et al., Imperfect forward secrecy: How Diffie-Hellman fails in practice, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.5-17, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01982426

T. Perrin, The Noise protocol framework, 2015.

V. Cheval and B. Blanchet, Proving more observational equivalences with ProVerif, International Conference on Principles of Security and Trust, pp.226-246, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00863377

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

M. Abadi, B. Blanchet, and C. Fournet, The applied pi calculus: Mobile values, new names, and secure communication, J. ACM, vol.65, issue.1, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01423924

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, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575923

K. Bhargavan, B. Blanchet, and N. Kobeissi, Verified models and reference implementations for the TLS 1.3 standard candidate, Security and Privacy (SP), 2017 IEEE Symposium on, pp.483-502, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575920

B. Schmidt, S. Meier, C. Cremers, and D. Basin, Automated analysis of Diffie-Hellman protocols and advanced security properties, IEEE Computer Security Foundations Symposium (CSF), pp.78-94, 2012.

J. Donenfeld and K. Milner, Formal verification of the WireGuard protocol, 2017.

A. Jason and . Donenfeld, WireGuard: next generation kernel network tunnel, 24th Annual Network and Distributed System Security Symposium, NDSS, 2017.

B. Dowling and K. G. Paterson, A cryptographic analysis of the WireGuard protocol, Cryptology ePrint Archive, 2018.

B. Lipp, B. Blanchet, and K. Bhargavan, A mechanised cryptographic proof of the WireGuard virtual private network protocol, IEEE European Symposium on Security and Privacy (EuroS&P), 2019.
URL : https://hal.archives-ouvertes.fr/hal-02100345

B. Blanchet, CryptoVerif: Computationally sound mechanized prover for cryptographic protocols, Dagstuhl seminar Formal Protocol Verification Applied, p.117, 2007.

G. Girol, Formalizing and verifying the security protocols from the noise framework, 2019.

K. Bhargavan, B. Bond, A. Delignat-lavaud, C. Fournet, C. Hawblitzel et al., Towards a verified, drop-in replacement of HTTPS, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01672707

N. Swamy, C. Hri?cu, C. Keller, A. Rastogi, A. Delignat-lavaud et al., Dependent types and multi-monadic effects in F ?, ACM SIGPLAN Notices, vol.51, pp.256-270, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01265793

M. Hamburg, The STROBE protocol framework. IACR Cryptology ePrint Archive, p.3, 2017.

D. Wong, Disco: Modern session encryption. Cryptology ePrint Archive, 2019.

M. Hall-andersen, D. Wong, N. Sullivan, and A. Chator, nQUIC: Noise-based QUIC packet protection, Proceedings of the Workshop on the Evolution, Performance, and Interoperability of QUIC, pp.22-28, 2018.

A. Langley, A. Riddoch, A. Wilk, A. Vicente, C. Krasic et al., The QUIC transport protocol: Design and internet-scale deployment, Proceedings of the Conference of the ACM Special Interest Group on Data Communication, pp.183-196, 2017.

P. Rogaway, Authenticated-encryption with associated-data, Ninth ACM Conference on Computer and Communications Security (CCS-9, pp.98-107, 2002.

H. Krawczyk, Cryptographic extraction and key derivation: The HKDF scheme, Advances in Cryptology (CRYPTO), pp.631-648, 2010.

D. J. Bernstein, Curve25519: New Diffie-Hellman speed records, Public Key Cryptography (PKC), pp.207-228, 2006.

J. Galt, cacophony: A library implementing the Noise protocol, 2019.

B. Beurdouche, K. Bhargavan, A. Delignat-lavaud, C. Fournet, M. Kohlweiss et al., A messy state of the union: Taming the composite state machines of TLS, IEEE Symposium on Security and Privacy (S&P), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01114250

J. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, HACL*: A verified modern cryptographic library, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp.1789-1806, 2017.

T. Pornin, BearSSL: a smaller SSL/TLS library, 2019.

, WebAssembly Core Specification, 2018.