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, p.11, 1993.

D. J. Bernstein, The Poly1305-AES message-authentication code, FSE 2005, vol.3557, p.11, 2005.

D. J. Bernstein, Curve25519: New Diffie-Hellman speed records, PKC 2006, vol.3958, pp.207-228, 2006.

. Inria,

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), p.37, 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), vol.3, p.31, 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, vol.3, p.4, 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, 2004.

B. Blanchet, Security protocol verification: Symbolic and computational models, Principles of Security and Trust, POST'12, vol.7215, p.37, 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, 2003.
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, vol.10403, 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, p.31, 2008.

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

C. Cremers and D. Jackson, Prime, order please! revisiting small subgroup and invalid curve attacks on protocols using Diffie-Hellman, IEEE CSF'19, 2019.

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, p.42, 2012.

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

J. A. Donenfeld and K. Milner, Formal verification of the WireGuard protocol, vol.20, p.37, 2018.

B. Dowling and K. G. Paterson, A cryptographic analysis of the WireGuard protocol, Applied Cryptography and Network Security, ACNS 2018, vol.10892, p.38, 1920.

G. , Formalizing and verifying the security protocols from the Noise framework, vol.37, p.38, 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, p.26, 2012.

S. Kent and K. Yao, Security Architecture for the Internet Protocol, IETF RFC, vol.4301, issue.3, 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, vol.37, p.42, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575923

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

H. Krawczyk and P. Eronen, HMAC-based extract-and-expand key derivation function (HKDF), IETF RFC, vol.5869, p.22, 2010.
DOI : 10.17487/rfc5869
URL : https://www.rfc-editor.org/rfc/pdfrfc/rfc5869.txt.pdf

A. Langley, M. Hamburg, and S. Turner, Elliptic curves for security, IETF RFC, vol.7748, p.17, 2016.
DOI : 10.17487/rfc7748
URL : https://www.rfc-editor.org/rfc/pdfrfc/rfc7748.txt.pdf

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

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, 2011.

M. Marlinspike and T. Perrin, The X3DH key agreement protocol, p.20, 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, p.11, 2018.
DOI : 10.17487/rfc8439
URL : https://www.rfc-editor.org/rfc/pdfrfc/rfc8439.txt.pdf

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

T. Perrin, The Noise protocol framework, vol.5, p.10, 2018.

. Inria,

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

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

M. Saarinen and J. Aumasson, The BLAKE2 cryptographic hash and message authentication code (MAC), IETF RFC, vol.7693, issue.9, 2015.

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

, D n respectively, and H(x) = H i (x) if x ? D i for some i ? n, and H(x) = H 0 (x) otherwise, ? the game G 0 in which H is a random oracle, and H i (x) =

, Proof of Lemma 3. Consider ? the game G 0 in which H 1 and H 2 are independent random oracles, and H (x) = H 1 (x) H 2 (x), and ? the game G 1 in which H is a random oracle that returns bitstrings of

, ? the game G 1 in which H 1 and H 2 are independent random oracles that return bitstrings of length l 1 and l ? l 1 respectively, and H(x) = H 1 (x) H 2 (x)

, It is easy to see that these two games are perfectly indistinguishable, which proves indifferentiability. (It is the same indistinguishability result as in Lemma, vol.1

, H n are independent random oracles; the simulator for hmac calls H 0 at most q H0 times, H 1 at most q H1 times via the second hole of S 2 , H i?1 and H i with the same arguments at most q Hi times via the (i + 1)-th hole of S 2 for 1 < i ? n, with q H0 + · · · + q Hn ? q hmac , and runs in time O

, there exist simulators S 4,j (1 ? j ? n) for H j such that G 3,n is perfectly indistinguishable from G 4 in which hmac = S 2, By Lemma, vol.3