Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS, IEEE Symposium on Security and Privacy (S&P), pp.98-113, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01102259
An attack on the Needham-Schroeder public-key authentication protocol, Information processing letters, vol.56, issue.3, 1995. ,
Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978. ,
Verified contributive channel bindings for compound authentication, Network and Distributed System Security Symposium (NDSS '15), 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01114248
A comprehensive symbolic analysis of TLS 1.3, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS '17, pp.1773-1788, 2017. ,
Imperfect forward secrecy: How Diffie-Hellman fails in practice, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.5-17, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01982426
The Noise protocol framework, 2015. ,
Proving more observational equivalences with ProVerif, International Conference on Principles of Security and Trust, pp.226-246, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00863377
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 applied pi calculus: Mobile values, new names, and secure communication, J. ACM, vol.65, issue.1, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01423924
Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach, IEEE European Symposium on Security and Privacy, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01575923
Verified models and reference implementations for the TLS 1.3 standard candidate, Security and Privacy (SP), 2017 IEEE Symposium on, pp.483-502, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01575920
Automated analysis of Diffie-Hellman protocols and advanced security properties, IEEE Computer Security Foundations Symposium (CSF), pp.78-94, 2012. ,
Formal verification of the WireGuard protocol, 2017. ,
WireGuard: next generation kernel network tunnel, 24th Annual Network and Distributed System Security Symposium, NDSS, 2017. ,
A cryptographic analysis of the WireGuard protocol, Cryptology ePrint Archive, 2018. ,
A mechanised cryptographic proof of the WireGuard virtual private network protocol, IEEE European Symposium on Security and Privacy (EuroS&P), 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02100345
CryptoVerif: Computationally sound mechanized prover for cryptographic protocols, Dagstuhl seminar Formal Protocol Verification Applied, p.117, 2007. ,
Formalizing and verifying the security protocols from the noise framework, 2019. ,
Towards a verified, drop-in replacement of HTTPS, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01672707
Dependent types and multi-monadic effects in F ?, ACM SIGPLAN Notices, vol.51, pp.256-270, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01265793
The STROBE protocol framework. IACR Cryptology ePrint Archive, p.3, 2017. ,
Disco: Modern session encryption. Cryptology ePrint Archive, 2019. ,
nQUIC: Noise-based QUIC packet protection, Proceedings of the Workshop on the Evolution, Performance, and Interoperability of QUIC, pp.22-28, 2018. ,
The QUIC transport protocol: Design and internet-scale deployment, Proceedings of the Conference of the ACM Special Interest Group on Data Communication, pp.183-196, 2017. ,
Authenticated-encryption with associated-data, Ninth ACM Conference on Computer and Communications Security (CCS-9, pp.98-107, 2002. ,
Cryptographic extraction and key derivation: The HKDF scheme, Advances in Cryptology (CRYPTO), pp.631-648, 2010. ,
Curve25519: New Diffie-Hellman speed records, Public Key Cryptography (PKC), pp.207-228, 2006. ,
cacophony: A library implementing the Noise protocol, 2019. ,
A messy state of the union: Taming the composite state machines of TLS, IEEE Symposium on Security and Privacy (S&P), 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01114250
HACL*: A verified modern cryptographic library, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp.1789-1806, 2017. ,
BearSSL: a smaller SSL/TLS library, 2019. ,
, WebAssembly Core Specification, 2018.