Web-based Attacks on Host-Proof Encrypted Storage. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud (WOOT, 2012)

Defensive JavaScript - Building and Verifying Secure Web Components. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Sergio Maffeis (FOSAD, 2013)

Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage. - Chetan Bansal; Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Sergio Maffeis (POST, 2013)

Language-based Defenses Against Untrusted Browser Origins. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Sergio Maffeis (USENIX Security Symposium, 2013)

Web PKI: Closing the Gap between Guidelines and Practices. - Antoine Delignat-Lavaud; Martín Abadi; Andrew Birrell; Ilya Mironov; Ted Wobber; Yinglian Xie (NDSS, 2014)

Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Alfredo Pironti 001; Pierre-Yves Strub (IEEE Symposium on Security and Privacy, 2014)

Discovering concrete attacks on website authorization by formal analysis. - Chetan Bansal; Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Sergio Maffeis (J. Comput. Secur., 2014)

Verified Contributive Channel Bindings for Compound Authentication. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Alfredo Pironti 001 (NDSS, 2015)

FLEXTLS: A Tool for Testing TLS Implementations. - Benjamin Beurdouche; Antoine Delignat-Lavaud; Nadim Kobeissi; Alfredo Pironti 001; Karthikeyan Bhargavan (WOOT, 2015)

Network-based Origin Confusion Attacks against HTTPS Virtual Hosting. - Antoine Delignat-Lavaud; Karthikeyan Bhargavan (WWW, 2015)

Transport Layer Security (TLS) Session Hash and Extended Master Secret Extension. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Alfredo Pironti 001; Adam Langley; Marsh Ray (RFC, 2015)

Formal Verification of Smart Contracts: Short Paper. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Anitha Gollamudi; Georges Gonthier; Nadim Kobeissi; Natalia Kulatova; Aseem Rastogi; Thomas Sibut-Pinote; Nikhil Swamy; Santiago Zanella-Béguelin (PLAS@CCS, 2016)

Dependent types and multi-monadic effects in F. - Nikhil Swamy; Catalin Hritcu; Chantal Keller; Aseem Rastogi; Antoine Delignat-Lavaud; Simon Forest; Karthikeyan Bhargavan; Cédric Fournet; Pierre-Yves Strub; Markulf Kohlweiss; Jean Karim Zinzindohoue; Santiago Zanella-Béguelin (POPL, 2016)

Cinderella: Turning Shabby X.509 Certificates into Elegant Anonymous Credentials with the Magic of Verifiable Computation. - Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Bryan Parno (IEEE Symposium on Security and Privacy, 2016)

Implementing and Proving the TLS 1.3 Record Layer. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Jianyang Pan; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin; Jean Karim Zinzindohoue (IACR Cryptol. ePrint Arch., 2016)

On the security of authentication protocols on the web. (La sécurité des protocoles d'authentification sur leWeb). - Antoine Delignat-Lavaud (2016)

Formal Modeling and Verification for Domain Validation and ACME. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Nadim Kobeissi (Financial Cryptography, 2017)

Everest: Towards a Verified, Drop-in Replacement of HTTPS. - Karthikeyan Bhargavan; Barry Bond; Antoine Delignat-Lavaud; Cédric Fournet; Chris Hawblitzel; Catalin Hritcu; Samin Ishtiaq; Markulf Kohlweiss; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

A messy state of the union: taming the composite state machines of TLS. - Benjamin Beurdouche; Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub; Jean Karim Zinzindohoue (Commun. ACM, 2017)

Verified Low-Level Programming Embedded in F*. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (CoRR, 2017)

Verified low-level programming embedded in F. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (Proc. ACM Program. Lang., 2017)

State Separation for Code-Based Game-Playing Proofs. - Chris Brzuska; Antoine Delignat-Lavaud; Cédric Fournet; Konrad Kohbrok; Markulf Kohlweiss (ASIACRYPT (3), 2018)

A Formal Treatment of Accountable Proxying Over TLS. - Karthikeyan Bhargavan; Ioana Boureanu; Antoine Delignat-Lavaud; Pierre-Alain Fouque; Cristina Onete (IEEE Symposium on Security and Privacy, 2018)

State-Separating Proofs: A Reduction Methodology for Real-World Protocols. - Chris Brzuska; Antoine Delignat-Lavaud; Konrad Kohbrok; Markulf Kohlweiss (IACR Cryptol. ePrint Arch., 2018)

EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. - Tahina Ramananandro; Antoine Delignat-Lavaud; Cédric Fournet; Nikhil Swamy; Tej Chajed; Nadim Kobeissi; Jonathan Protzenko (USENIX Security Symposium, 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Natalia Kulatova; Tahina Ramananandro; et al. (SP, 2020)

A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. - Antoine Delignat-Lavaud; Cédric Fournet; Bryan Parno; Jonathan Protzenko; Tahina Ramananandro; Jay Bosamiya; Joseph Lallemand; Itsaka Rakotonirina; Yi Zhou 025 (IACR Cryptol. ePrint Arch., 2020)

Toward confidential cloud computing. - Mark Russinovich; Manuel Costa; Cédric Fournet; David Chisnall; Antoine Delignat-Lavaud; Sylvan Clebsch; Kapil Vaswani; Vikas Bhatia (Commun. ACM, 2021)

PAC: Practical Accountability for CCF. - Alex Shamis; Peter R. Pietzuch; Miguel Castro 001; Edward Ashton; Amaury Chamayou; Sylvan Clebsch; Antoine Delignat-Lavaud; Cédric Fournet; Matthew Kerner; Julien Maffre; Manuel Costa; Mark Russinovich (CoRR, 2021)

Key-schedule Security for the TLS 1.3 Standard. - Chris Brzuska; Antoine Delignat-Lavaud; Christoph Egger 001; Cédric Fournet; Konrad Kohbrok; Markulf Kohlweiss (IACR Cryptol. ePrint Arch., 2021)

Toward Confidential Cloud Computing: Extending hardware-enforced cryptographic protection to data while in use. - Mark Russinovich; Manuel Costa; Cédric Fournet; David Chisnall; Antoine Delignat-Lavaud; Sylvan Clebsch; Kapil Vaswani; Vikas Bhatia (ACM Queue, 2021)

IA-CCF: Individual Accountability for Permissioned Ledgers. - Alex Shamis; Peter R. Pietzuch; Burcu Canakci; Miguel Castro 001; Cédric Fournet; Edward Ashton; Amaury Chamayou; Sylvan Clebsch; Antoine Delignat-Lavaud; Matthew Kerner; Julien Maffre; Olga Vrousgou; et al. (NSDI, 2022)

Dropbear: Machine Learning Marketplaces made Trustworthy with Byzantine Model Agreement. - Alex Shamis; Peter R. Pietzuch; Antoine Delignat-Lavaud; Andrew Paverd; Manuel Costa (CoRR, 2022)

ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. - Haobin Ni; Antoine Delignat-Lavaud; Cédric Fournet; Tahina Ramananandro; Nikhil Swamy (CPP, 2023)

Confidential Consortium Framework: Secure Multiparty Applications with Confidentiality, Integrity, and High Availability. - Heidi Howard; Fritz Alder; Edward Ashton; Amaury Chamayou; Sylvan Clebsch; Manuel Costa; Antoine Delignat-Lavaud; Cédric Fournet; Andrew Jeffery; Matthew Kerner; Fotios Kounelis; Markus A. Kuppe; et al. (Proc. VLDB Endow., 2023)

Why Should I Trust Your Code?: Confidential computing enables users to authenticate code running in TEEs, but users also need evidence this code is trustworthy. - Antoine Delignat-Lavaud; Cédric Fournet; Kapil Vaswani; Sylvan Clebsch; Maik Riechert; Manuel Costa; Mark Russinovich (ACM Queue, 2023)

Why Should I Trust Your Code? - Antoine Delignat-Lavaud; Cédric Fournet; Kapil Vaswani; Sylvan Clebsch; Maik Riechert; Manuel Costa; Mark Russinovich (Commun. ACM, 2024)

Transparent Attested DNS for Confidential Computing Services. - Antoine Delignat-Lavaud; Cédric Fournet; Kapil Vaswani; Manuel Costa; Sylvan Clebsch; Christoph M. Wintersteiger (CoRR, 2025)