S. Kent and K. Yao, Security Architecture for the Internet Protocol, 2005.

E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.3, IETF RFC, vol.8446, 2018.

K. Bhargavan and G. Leurent, On the practical (in-)security of 64-bit block ciphers: Collision attacks on HTTP over TLS and OpenVPN, ACM CCS'16, pp.456-467, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01404208

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, pp.535-552, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01114250

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

M. Marlinspike and T. Perrin, The X3DH key agreement protocol, 2016.

T. Perrin, The Noise protocol framework, 2018.

J. A. Donenfeld, we use the up-to-date whitepaper version for our analysis, Network and Distributed System Security Symposium, 2017.

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

S. Meier, B. Schmidt, C. Cremers, and D. A. Basin, The TAMARIN prover for the symbolic analysis of security protocols, Computer Aided Verification, CAV'13, ser, vol.8044, pp.696-701, 2013.

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

B. Dowling and K. G. Paterson, A cryptographic analysis of the WireGuard protocol, Applied Cryptography and Network Security, ACNS 2018, ser. LNCS, vol.10892, pp.3-21, 2018.

B. Blanchet, Computationally sound mechanized proofs of correspondence assertions, IEEE CSF'07, vol.5, pp.97-111, 2007.

B. Lipp, B. Blanchet, and K. Bhargavan, A mechanised cryptographic proof of the WireGuard virtual private network protocol, Inria, Research report, vol.9269, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02396640

A. Langley, M. Hamburg, and S. Turner, Elliptic curves for security, 2016.

M. Saarinen and J. Aumasson, The BLAKE2 cryptographic hash and message authentication code (MAC), 2015.

Y. Nir and A. Langley, ChaCha20 and Poly1305 for IETF Protocols, IETF RFC, vol.8439, 2018.

D. J. Bernstein, Extending the Salsa20 nonce, 2011.

H. Krawczyk and P. Eronen, HMAC-based extract-and-expand key derivation function (HKDF), 2010.

M. Bellare and P. Rogaway, Random oracles are practical: a paradigm for designing efficient protocols, ACM CCS'93, pp.62-73, 1993.

A. Luykx, B. Mennink, and S. Neves, Security analysis of BLAKE2's modes of operation, IACR Transactions on Symmetric Cryptology, vol.2016, issue.1, pp.158-176, 2016.

M. Bellare and C. Namprempre, Authenticated encryption: Relations among notions and analysis of the generic composition paradigm, ASIACRYPT'00, ser, pp.531-545, 1976.

G. Procter, A security analysis of the composition of ChaCha20 and Poly1305, 2014.

D. J. Bernstein, The Poly1305-AES message-authentication code, FSE 2005, ser. LNCS, vol.3557, pp.32-49, 2005.

T. Okamoto and D. , The gap-problems: a new class of problems for the security of cryptographic schemes, PKC 2001, ser. LNCS, pp.104-118, 1992.

J. Brendel, M. Fischlin, F. Günther, and C. Janson, PRF-ODH: Relations, instantiations, and impossibility results, CRYPTO 2017, ser. LNCS, vol.10403, pp.651-681, 2017.

J. Coron, Y. Dodis, C. Malinaud, and P. Puniya, Merkle-Damgård revisited: How to construct a hash function, CRYPTO 2005, ser. LNCS, vol.3621, pp.430-448, 2005.

N. Kobeissi, K. Bhargavan, and B. Blanchet, Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach, IEEE EuroS&P'17, pp.435-450, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575923

J. Aumasson, S. Neves, Z. Wilcox-o'hearn, and C. Winnerlein, BLAKE2: Simpler, smaller, fast as MD5, Applied Cryptography and Network Security, ser. LNCS, vol.7954, pp.119-135, 2013.

Y. Dodis, T. Ristenpart, J. Steinberger, and S. Tessaro, To hash or not to hash again? (in)differentiability results for H 2 and HMAC, CRYPTO 2012, ser. LNCS, vol.7417, pp.348-366, 2012.

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

L. Chen and Q. Tang, Bilateral unknown key-share attacks in key agreement protocols, Journal of Universal Computer Science, vol.14, issue.3, pp.416-440, 2008.

B. Blanchet, Security protocol verification: Symbolic and computational models, Principles of Security and Trust, POST'12, ser, vol.7215, pp.3-29, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00863388

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

N. Kobeissi, G. Nicolas, and K. Bhargavan, Noise Explorer: Fully automated modeling and verification for arbitrary Noise protocols, IEEE EuroS&P, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01948964

A. Suter-dörig, Formalizing and verifying the security protocols from the Noise framework, 2018.

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