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