The Village Telephone System: A Case Study in Formal Software Engineering. - Karthikeyan Bhargavan; Carl A. Gunter; Elsa L. Gunter; Michael Jackson 001; Davor Obradovic; Pamela Zave (TPHOLs, 1998)

Fault origin adjudication. - Karthikeyan Bhargavan; Carl A. Gunter; Davor Obradovic (FMSP, 2000)

Routing Information Protocol in HOL/SPIN. - Karthikeyan Bhargavan; Carl A. Gunter; Davor Obradovic (TPHOLs, 2000)

What packets may come: automata for network monitoring. - Karthikeyan Bhargavan; Satish Chandra 001; Peter J. McCann; Carl A. Gunter (POPL, 2001)

Requirements for a Practical Network Event Recognition Language. - Karthikeyan Bhargavan; Carl A. Gunter (RV@FLoC, 2002)

Formal verification of standards for distance vector routing protocols. - Karthikeyan Bhargavan; Davor Obradovic; Carl A. Gunter (J. ACM, 2002)

Verisim: Formal Analysis of Network Simulations. - Karthikeyan Bhargavan; Carl A. Gunter; Moonjoo Kim 001; Insup Lee 001; Davor Obradovic; Oleg Sokolsky; Mahesh Viswanathan 001 (IEEE Trans. Software Eng., 2002)

TulaFale: A Security Tool for Web Services. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001; Riccardo Pucella (FMCO, 2003)

Verifying policy-based security for web services. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001 (CCS, 2004)

A Constraint-Based Formalism for Consistency in Replicated Systems. - Marc Shapiro 001; Karthikeyan Bhargavan; Nishith Krishna (OPODIS, 2004)

Brief announcement: exploring the consistency problem space. - Nishith Krishna; Marc Shapiro 001; Karthikeyan Bhargavan (PODC, 2005)

An advisor for web services security policies. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001; Greg O'Shea (SWS, 2005)

Network Event Recognition. - Karthikeyan Bhargavan; Carl A. Gunter (Formal Methods Syst. Des., 2005)

A semantics for web services authentication. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001 (Theor. Comput. Sci., 2005)

Verified Reference Implementations of WS-Security Protocols. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001 (WS-FM, 2006)

Secure Implementations for Typed Session Abstractions. - Ricardo Corin; Pierre-Malo Deniélou; Cédric Fournet; Karthikeyan Bhargavan; James J. Leifer (CSF, 2007)

Service Combinators for Farming Virtual Machines. - Karthikeyan Bhargavan; Andrew D. Gordon 001; Iman Narasamdya (TGC, 2007)

Secure sessions for Web services. - Karthikeyan Bhargavan; Ricardo Corin; Cédric Fournet; Andrew D. Gordon 001 (ACM Trans. Inf. Syst. Secur., 2007)

Cryptographically verified implementations for TLS. - Karthikeyan Bhargavan; Cédric Fournet; Ricardo Corin; Eugen Zalinescu (CCS, 2008)

Verified implementations of the information card federated identity-management protocol. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001; Nikhil Swamy (AsiaCCS, 2008)

A secure compiler for session abstractions. - Ricardo Corin; Pierre-Malo Deniélou; Cédric Fournet; Karthikeyan Bhargavan; James J. Leifer (J. Comput. Secur., 2008)

Verifying policy-based web services security. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001 (ACM Trans. Program. Lang. Syst., 2008)

Verified interoperable implementations of security protocols. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001; Stephen Tse (ACM Trans. Program. Lang. Syst., 2008)

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. - Karthikeyan Bhargavan; Ricardo Corin; Pierre-Malo Deniélou; Cédric Fournet; James J. Leifer (CSF, 2009)

A compositional theory for STM Haskell. - Johannes Borgström; Karthikeyan Bhargavan; Andrew D. Gordon 001 (Haskell, 2009)

Typechecking Higher-Order Security Libraries. - Karthikeyan Bhargavan; Cédric Fournet; Nataliya Guts (APLAS, 2010)

Modular verification of security protocol code by typing. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001 (POPL, 2010)

Cryptographic Verification by Typing for a Sample Protocol Implementation. - Cédric Fournet; Karthikeyan Bhargavan; Andrew D. Gordon 001 (FOSAD, 2011)

Refinement types for secure implementations. - Jesper Bengtson; Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001; Sergio Maffeis (ACM Trans. Program. Lang. Syst., 2011)

Discovering Concrete Attacks on Website Authorization by Formal Analysis. - Chetan Bansal; Karthikeyan Bhargavan; Sergio Maffeis (CSF, 2012)

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

Verified Cryptographic Implementations for TLS. - Karthikeyan Bhargavan; Cédric Fournet; Ricardo Corin; Eugen Zalinescu (ACM Trans. Inf. Syst. Secur., 2012)

Towards Unified Authorization for Android. - Michael J. May; Karthikeyan Bhargavan (ESSoS, 2013)

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)

Implementing TLS with Verified Cryptographic Security. - Karthikeyan Bhargavan; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub (IEEE Symposium on Security and Privacy, 2013)

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

Secure distributed programming with value-dependent types. - Nikhil Swamy; Juan Chen 002; Cédric Fournet; Pierre-Yves Strub; Karthikeyan Bhargavan; Jean Yang 001 (J. Funct. Program., 2013)

Gradual typing embedded securely in JavaScript. - Nikhil Swamy; Cédric Fournet; Aseem Rastogi; Karthikeyan Bhargavan; Juan Chen 002; Pierre-Yves Strub; Gavin M. Bierman (POPL, 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)

Proving the TLS Handshake Secure (as it is). - Karthikeyan Bhargavan; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 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)

A Verified Extensible Library of Elliptic Curves. - Jean Karim Zinzindohoue; Evmorfia-Iro Bartzia; Karthikeyan Bhargavan (CSF, 2016)

Transcript Collision Attacks: Breaking Authentication in TLS, IKE and SSH. - Karthikeyan Bhargavan; Gaëtan Leurent (NDSS, 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)

Downgrade Resilience in Key-Exchange Protocols. - Karthikeyan Bhargavan; Christina Brzuska; Cédric Fournet; Matthew Green 001; Markulf Kohlweiss; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 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 Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN. - Karthikeyan Bhargavan; Gaëtan Leurent (IACR Cryptol. ePrint Arch., 2016)

miTLS: Verifying Protocol Implementations against Real-World Attacks. - Karthikeyan Bhargavan; Cédric Fournet; Markulf Kohlweiss (IEEE Secur. Priv., 2016)

Content delivery over TLS: a cryptographic analysis of keyless SSL. - Karthikeyan Bhargavan; Ioana Boureanu; Pierre-Alain Fouque; Cristina Onete; Benjamin Richard (EuroS&P, 2017)

Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. - Nadim Kobeissi; Karthikeyan Bhargavan; Bruno Blanchet (EuroS&P, 2017)

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)

Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. - Karthikeyan Bhargavan; Bruno Blanchet; Nadim Kobeissi (IEEE Symposium on Security and Privacy, 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)

HACL*: A Verified Modern Cryptographic Library. - Jean Karim Zinzindohoué; Karthikeyan Bhargavan; Jonathan Protzenko; Benjamin Beurdouche (IACR Cryptol. ePrint Arch., 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)

hacspec: Towards Verifiable Crypto Standards. - Karthikeyan Bhargavan; Franziskus Kiefer; Pierre-Yves Strub (SSR, 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)

Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols. - Nadim Kobeissi; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2018)

Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols. - Nadim Kobeissi; Georgio Nicolas; Karthikeyan Bhargavan (EuroS&P, 2019)

A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. - Benjamin Lipp 001; Bruno Blanchet; Karthikeyan Bhargavan (EuroS&P, 2019)

Practical Formal Methods for Real World Cryptography (Invited Talk). - Karthikeyan Bhargavan; Prasad Naldurg (FSTTCS, 2019)

Imperfect forward secrecy: how Diffie-Hellman fails in practice. - David Adrian; Karthikeyan Bhargavan; Zakir Durumeric; Pierrick Gaudry; Matthew Green 001; J. Alex Halderman; Nadia Heninger; Drew Springall; Emmanuel Thomé; Luke Valenta; Benjamin VanderSloot; Eric Wustrow; et al. (Commun. ACM, 2019)

SoK: Computer-Aided Cryptography. - Manuel Barbosa; Gilles Barthe; Karthikeyan Bhargavan; Bruno Blanchet; Cas Cremers; Kevin Liao; Bryan Parno (IACR Cryptol. ePrint Arch., 2019)

Formally Verified Cryptographic Web Applications in WebAssembly. - Jonathan Protzenko; Benjamin Beurdouche; Denis Merigoux; Karthikeyan Bhargavan (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; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms). - Marina Polubelova; Karthikeyan Bhargavan; Jonathan Protzenko; Benjamin Beurdouche; Aymeric Fromherz; Natalia Kulatova; Santiago Zanella-Béguelin (CCS, 2020)

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)

HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms). - Marina Polubelova; Karthikeyan Bhargavan; Jonathan Protzenko; Benjamin Beurdouche; Aymeric Fromherz; Natalia Kulatova; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2020)

A Tutorial-Style Introduction to DY*. - Karthikeyan Bhargavan; Abhishek Bichhawat; Quoc Huy Do 001; Pedram Hosseyni; Ralf Küsters; Guido Schmitz; Tim Würtele (Protocols, Strands, and Logic, 2021)

DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. - Karthikeyan Bhargavan; Abhishek Bichhawat; Quoc Huy Do 001; Pedram Hosseyni; Ralf Küsters; Guido Schmitz; Tim Würtele (EuroS&P, 2021)

An In-Depth Symbolic Security Analysis of the ACME Standard. - Karthikeyan Bhargavan; Abhishek Bichhawat; Quoc Huy Do 001; Pedram Hosseyni; Ralf Küsters; Guido Schmitz; Tim Würtele (IACR Cryptol. ePrint Arch., 2021)

A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello. - Karthikeyan Bhargavan; Vincent Cheval; Christopher A. Wood (CCS, 2022)

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations. - Son Ho; Jonathan Protzenko; Abhishek Bichhawat; Karthikeyan Bhargavan (SP, 2022)

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version). - Son Ho; Jonathan Protzenko; Abhishek Bichhawat; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2022)

TreeSync: Authenticated Group Management for Messaging Layer Security. - Théophile Wallez; Jonathan Protzenko; Benjamin Beurdouche; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2022)

Hybrid Public Key Encryption. - Richard L. Barnes; Karthikeyan Bhargavan; Benjamin Lipp 001; Christopher A. Wood (RFC, 2022)

Layered Symbolic Security Analysis in $ textsf {DY}^ star $. - Karthikeyan Bhargavan; Abhishek Bichhawat; Pedram Hosseyni; Ralf Küsters; Klaas Pruiksma; Guido Schmitz; Clara Waldmann; Tim Würtele (ESORICS (3), 2023)

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 (EuroS&P, 2023)

Layered Symbolic Security Analysis in DY$^ star$. - Karthikeyan Bhargavan; Abhishek Bichhawat; Pedram Hosseyni; Ralf Küsters; Klaas Pruiksma; Guido Schmitz; Clara Waldmann; Tim Würtele (IACR Cryptol. ePrint Arch., 2023)

Comparse: Provably Secure Formats for Cryptographic Protocols. - Théophile Wallez; Jonathan Protzenko; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2023)

Foundations of WebAssembly (Dagstuhl Seminar 23101). - Karthikeyan Bhargavan; Jonathan Protzenko; Andreas Rossberg; Deian Stefan (Dagstuhl Reports, 2023)

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)

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 (IACR Cryptol. ePrint Arch., 2025)

Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust. - Karthikeyan Bhargavan; Lasse Letager Hansen; Franziskus Kiefer; Jonas Schneider-Bensch; Bas Spitters (IACR Cryptol. ePrint Arch., 2025)

TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security. - Théophile Wallez; Jonathan Protzenko; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2025)

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 Trans. Cryptogr. Hardw. Embed. Syst., 2025)

A Mechanically Verified Garbage Collector for OCaml. - Sheera Shamsu; Dipesh Kafle; Dhruv Maroo; Kartik Nagar; Karthikeyan Bhargavan; K. C. Sivaramakrishnan (J. Autom. Reason., 2025)