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

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

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

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

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

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 S&P (Oakland), pp.535-552, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01114250

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

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 (Oakland), pp.98-113, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102259

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. Blanchet, Computationally sound mechanized proofs of correspondence assertions, IEEE CSF'07, pp.97-111, 2007.

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.

B. Blanchet, Security protocol verification: Symbolic and computational models, Principles of Security and Trust, POST'12, vol.7215, pp.3-29, 2012.
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, vol.1, issue.1-2, pp.1-135, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01423760

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

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.

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

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, vol.7417, pp.348-366, 2012.

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

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, vol.10892, pp.3-21, 2018.

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

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

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

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

N. Kobeissi, G. Nicholas, 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

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

A. Langley, M. Hamburg, and S. Turner, Elliptic curves for security, IETF RFC, vol.7748, 2016.

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. Marlinspike and T. Perrin, The X3DH key agreement protocol, 2016.

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, vol.8044, pp.696-701, 2013.

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

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

T. Perrin, The Noise protocol framework, 2018.

G. Procter, A security analysis of the composition of ChaCha20 and Poly1305. Cryptology ePrint Archive, vol.613, 2014.

S. Kent and K. Yao, Security Architecture for the Internet Protocol, IETF RFC, vol.4301, 2005.

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

A. Suter-dörig, Formalizing and verifying the security protocols from the Noise framework. Bachelor's thesis, ETH Zürich, 2018.