Cryspen is deeply committed to cutting-edge research in formal verification tools and provably secure cryptographic solutions. We engage in long-term collaborations with universities and research institutes, and we seek to bridge the gap between academic research and their industrial application, allowing us to bring state-of-the-art research results directly into all our products and services.

Presentations

• 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)
• Real World Post Quantum Cryptography 2024: Verified ML-KEM in Rust and C using hax. Franziskus Kiefer. (Slides
• Open Source Crypto Workshop 2024: Cryptography with Formal Guarantees using hax. Franziskus Kiefer. (Slides, Video)
• MatchPoints 2024: High Assurance Post Quantum Cryptography. Karthikeyan Bhargavan. (Slides)

Papers

2025

• 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) (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)
• Public Key Linting for ML-KEM and ML-DSA. Evangelos Karatsiolis, Franziskus Kiefer, Juliane Krämer, Mirjam Loiero, Christian Tobias, Maximiliane Weishäupl. Workshop on Secure Protocol Implementations in the Quantum Era (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. 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)