Research
Pereq's publications and talks.
We work with our colleagues in academia and industry to extend the state-of-the-art in software verification and security analysis. We regularly publish and present our research in peer-reviewed conferences and workshops.
Presentations
- Software Verification in Lean 2026: Verifying Cryptographic Applications: Challenges and Opportunities. Karthikeyan Bhargavan. (Slides, Workshop)
- Dafny 2026 (POPL 2026): Software Verification meets Real-World Cryptography (Keynote). Karthikeyan Bhargavan. (Slides, Video, Workshop)
- PQCSA Workshop 2025 (co-located with escar Europe): High-Assurance Post-Quantum Cryptography for Security-Critical Applications (Keynote). Karthikeyan Bhargavan. (Slides, Video, Workshop)
- Real World Crypto 2025: Using Formally Verified Post-Quantum Algorithms at Scale. Lucas Franceschino with Andres Erbsen. (Slides, Video)
- VSTTE 2024: High Assurance Post Quantum Cryptography (Invited Talk). Karthikeyan Bhargavan. (Slides)
- CRYPTO 2024: Formal Methods for Cryptography: protocols, standards, implementations (Invited Talk). Karthikeyan Bhargavan. (Slides, Video)
- Real World Crypto 2024: An Analysis of Signal’s PQXDH. Karthikeyan Bhargavan with Rolfe Schmidt. (Slides, Video)
- NIST Workshop on Formal Methods within Certification Programs 2024: Formal Specifications for Certifiable Cryptography. Karthikeyan Bhargavan. (Slides)
- RustVerify 2024: Enabling High Assurance Cryptographic Software. Jonas Schneider-Bensch. (Slides)
- MatchPoints 2024: High Assurance Post Quantum Cryptography. Karthikeyan Bhargavan. (Slides)
Papers
2026
- Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software. Danel Ahman, Karthikeyan Bhargavan, Barry Bond, Jay Bosamiya, Christopher Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Aymeric Fromherz, Sydney Gibson, Chris Hawblitzel, Cătălin Hrițcu, Markulf Kohlweiss, Guido Martínez, Haobin Ni, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Exequiel Rivas, Nikhil Swamy and Santiago Zanella-Béguelin. ACM Transactions on Programming Languages and Systems, Volume 48, Issue 2. June 2026. (Paper)
- embedded-cal: A Formally Verified Cryptographic Provider for Embedded Platforms. Elsa López Pérez, William Takeshi Pereira, Thomas Watteyne, Christian Amsüss, Franziskus Kiefer, Jonas Schneider-Bensch, Karthikeyan Bhargavan, Mališa Vučinić. International Workshop on Security, Privacy and Trust in the Internet of Things (SPT-IoT), IEEE PerCom 2026 Awarded the SPT-IoT 2026 Best Paper Award. (Paper)
2025
- Secure Satellite Software-Defined Payloads with High-Assurance Post-Quantum Cryptography. Karthikeyan Bhargavan, Thomas Gazagnaire, Franziskus Kiefer, Virgile Robles. Security for Space Systems (3S) 2025 (Paper)
- Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust. Karthikeyan Bhargavan, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, Bas Spitters. ACM SIGSAC Conference on Computer and Communications Security (CCS) 2025 (Paper)
- A Mechanically Verified Garbage Collector for OCaml. Sheera Shamsu, Dipesh Kafle, Dhruv Maroo, Kartik Nagar, Karthikeyan Bhargavan, K. C. Sivaramakrishnan. Journal of Automated Reasoning. 69(2): 11 (2025). (Paper)
- KyberSlash: Exploiting secret-dependent division timings in Kyber implementations.
Daniel J. Bernstein, Karthikeyan Bhargavan, Shivam Bhasin, Anupam Chattopadhyay, Tee Kiah Chia, Matthias J. Kannwischer, Franziskus Kiefer, Thales B. Paiva, Prasanna Ravi, Goutam Tamvada. IACR Transactions on Cryptographic Hardware and Embedded Systems. 2025(2): 209-234 (2025) Awarded the CHES 2025 Best Paper Award. (Paper) - TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security. Theophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan. Symposium on Security and Privacy: 4375-4390 (2025) (Paper)
2024
- hax: Verifying Security-Critical Rust Software Using Multiple Provers. Karthikeyan Bhargavan, Maxime Buyse, Lucas Franceschino, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, Bas Spitters. Verified Software. Theories, Tools and Experiments (VSTTE) 2024: 96-119. (Paper)
- Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt: USENIX Security Symposium 2024 (Paper)
2023
- Comparse: Provably Secure Formats for Cryptographic Protocols. Theophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan. ACM SIGSAC Conference on Computer and Communications Security (CCS) 2023: 564-578. (Paper)
- Layered Symbolic Security Analysis in DY* Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Kuesters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, Tim Wuertele. ESORICS (3) 2023: 3-21 (Paper)
- From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake. Daniel De Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan. IEEE European Symposium on Security and Privacy (EuroS&P) 2023: 707-723. (Paper)
- TreeSync: Authenticated Group Management for Messaging Layer Security. Theophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan. USENIX Security Symposium 2023: 1217-1233. Awarded the Internet Defense Prize and a Distinguished Paper Award. (Paper)
2022
- A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello. Karthikeyan Bhargavan, Vincent Cheval, Christopher A. Wood. ACM SIGSAC Conference on Computer and Communications Security (CCS) 2022: 365-379. (Paper)
- Hybrid Public Key Encryption. Richard L. Barnes, Karthikeyan Bhargavan, Benjamin Lipp, Christopher A. Wood. IETF RFC 9180: 1-107 (2022) (Standard)
- Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations. Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan. IEEE Symposium on Security and Privacy (S&P) 2022: 107-124. (Paper)