BLAKE2: Simpler, smaller, fast as MD5, Applied Cryptography and Network Security, vol.7954, pp.119-135, 2013. ,
Authenticated encryption: Relations among notions and analysis of the generic composition paradigm, ASIACRYPT'00, vol.1976, pp.531-545, 2000. ,
Random oracles are practical: a paradigm for designing efficient protocols, ACM CCS'93, pp.62-73, 1993. ,
The Poly1305-AES message-authentication code, FSE 2005, vol.3557, pp.32-49, 2005. ,
Extending the Salsa20 nonce, 2011. ,
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
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
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
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
Computationally sound mechanized proofs of correspondence assertions, IEEE CSF'07, pp.97-111, 2007. ,
A computationally sound mechanized prover for security protocols, IEEE Transactions on Dependable and Secure Computing, vol.5, issue.4, pp.193-207, 2008. ,
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
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
PRF-ODH: Relations, instantiations, and impossibility results, CRYPTO 2017, volume 10403 of LNCS, pp.651-681, 2017. ,
Bilateral unknown key-share attacks in key agreement protocols, Journal of Universal Computer Science, vol.14, issue.3, pp.416-440, 2008. ,
Merkle-Damgård revisited: How to construct a hash function, CRYPTO 2005, vol.3621, pp.430-448, 2005. ,
To hash or not to hash again? (in)differentiability results for H 2 and HMAC, CRYPTO 2012, vol.7417, pp.348-366, 2012. ,
We use the up-to-date whitepaper version for our analysis, Network and Distributed System Security Symposium, 2017. ,
Formal verification of the WireGuard protocol, 2018. ,
A cryptographic analysis of the WireGuard protocol, Applied Cryptography and Network Security, ACNS 2018, vol.10892, pp.3-21, 2018. ,
The Transport Layer Security (TLS) Protocol Version 1.3, 2018. IETF RFC 8446 ,
Formalizing and verifying the security protocols from the Noise framework, 2019. ,
On the security of TLS-DHE in the standard model, CRYPTO 2012, vol.7417, pp.273-293, 2012. ,
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
Noise Explorer: Fully automated modeling and verification for arbitrary Noise protocols, IEEE EuroS&P, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01948964
HMAC-based extract-and-expand key derivation function (HKDF) ,
Elliptic curves for security, IETF RFC, vol.7748, 2016. ,
Security analysis of BLAKE2's modes of operation, IACR Transactions on Symmetric Cryptology, vol.2016, issue.1, pp.158-176, 2016. ,
The X3DH key agreement protocol, 2016. ,
The TAMARIN prover for the symbolic analysis of security protocols, Computer Aided Verification, CAV'13, vol.8044, pp.696-701, 2013. ,
ChaCha20 and Poly1305 for IETF Protocols, IETF RFC, vol.8439, 2018. ,
The gap-problems: a new class of problems for the security of cryptographic schemes, PKC 2001, volume 1992 of LNCS, pp.104-118, 2001. ,
The Noise protocol framework, 2018. ,
A security analysis of the composition of ChaCha20 and Poly1305. Cryptology ePrint Archive, vol.613, 2014. ,
Security Architecture for the Internet Protocol, IETF RFC, vol.4301, 2005. ,
The BLAKE2 cryptographic hash and message authentication code (MAC) ,
Formalizing and verifying the security protocols from the Noise framework. Bachelor's thesis, ETH Zürich, 2018. ,