Karthikeyan Bhargavan

ORCID

Publication Activity (10 Years)

Years Active: 1998-2024
Publications (10 Years): 54

Top Venues

IACR Cryptol. ePrint Arch.

IEEE Symposium on Security and Privacy

CCS

EuroS&P

Publications

Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt
Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. USENIX Security Symposium (2024)
Daniel J. Bernstein, Karthikeyan Bhargavan, Shivam Bhasin, Anupam Chattopadhyay, Tee Kiah Chia, Matthias J. Kannwischer, Franziskus Kiefer, Thales Paiva, Prasanna Ravi, Goutam Tamvada
KyberSlash: Exploiting secret-dependent division timings in Kyber implementations. IACR Cryptol. ePrint Arch. 2024 (2024)
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
Comparse: Provably Secure Formats for Cryptographic Protocols. IACR Cryptol. ePrint Arch. 2023 (2023)
Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, Deian Stefan
Foundations of WebAssembly (Dagstuhl Seminar 23101). Dagstuhl Reports 13 (3) (2023)
Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Küsters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, Tim Würtele
Layered Symbolic Security Analysis in $\textsf {DY}^\star $. ESORICS (3) (2023)
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
Comparse: Provably Secure Formats for Cryptographic Protocols. CCS (2023)
Daniel De Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan
From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake. CoRR (2023)
Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Küsters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, Tim Würtele
Layered Symbolic Security Analysis in DY$^\star$. IACR Cryptol. ePrint Arch. 2023 (2023)
Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan
TreeSync: Authenticated Group Management for Messaging Layer Security. USENIX Security Symposium (2023)
Daniel De Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan
From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake. EuroS&P (2023)
Karthikeyan Bhargavan, Vincent Cheval, Christopher A. Wood
A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello. CCS (2022)
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations. IEEE Symposium on Security and Privacy (2022)
Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan
TreeSync: Authenticated Group Management for Messaging Layer Security. IACR Cryptol. ePrint Arch. 2022 (2022)
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version). IACR Cryptol. ePrint Arch. 2022 (2022)
Richard L. Barnes, Karthikeyan Bhargavan, Benjamin Lipp, Christopher A. Wood
Hybrid Public Key Encryption. RFC 9180 (2022)
Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele
A Tutorial-Style Introduction to DY*. Protocols, Strands, and Logic (2021)
Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele
An In-Depth Symbolic Security Analysis of the ACME Standard. CCS (2021)
Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele
An In-Depth Symbolic Security Analysis of the ACME Standard. IACR Cryptol. ePrint Arch. 2021 (2021)
Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele
DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. EuroS&P (2021)
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella Béguelin
HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms). CCS (2020)
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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. IEEE Symposium on Security and Privacy (2020)
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella Béguelin
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms). IACR Cryptol. ePrint Arch. 2020 (2020)
David Adrian, Karthikeyan Bhargavan, Zakir Durumeric, Pierrick Gaudry, Matthew Green, J. Alex Halderman, Nadia Heninger, Drew Springall, Emmanuel Thomé, Luke Valenta, Benjamin VanderSloot, Eric Wustrow, Santiago Zanella Béguelin, Paul Zimmermann
Imperfect forward secrecy: how Diffie-Hellman fails in practice. Commun. ACM 62 (1) (2019)
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, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. IACR Cryptol. ePrint Arch. 2019 (2019)
Nadim Kobeissi, Georgio Nicolas, Karthikeyan Bhargavan
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols. EuroS&P (2019)
Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno
SoK: Computer-Aided Cryptography. IACR Cryptol. ePrint Arch. 2019 (2019)
Karthikeyan Bhargavan, Prasad Naldurg
Practical Formal Methods for Real World Cryptography (Invited Talk). FSTTCS (2019)
Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan
A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. EuroS&P (2019)
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
Formally Verified Cryptographic Web Applications in WebAssembly. IEEE Symposium on Security and Privacy (2019)
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
Formally Verified Cryptographic Web Applications in WebAssembly. IACR Cryptol. ePrint Arch. 2019 (2019)
Karthikeyan Bhargavan, Franziskus Kiefer, Pierre-Yves Strub
hacspec: Towards Verifiable Crypto Standards. SSR (2018)
Karthikeyan Bhargavan, Ioana Boureanu, Antoine Delignat-Lavaud, Pierre-Alain Fouque, Cristina Onete
A Formal Treatment of Accountable Proxying Over TLS. IEEE Symposium on Security and Privacy (2018)
Nadim Kobeissi, Karthikeyan Bhargavan
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols. IACR Cryptol. ePrint Arch. 2018 (2018)
Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi
Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. IEEE Symposium on Security and Privacy (2017)
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin, Karthikeyan Bhargavan, Jianyang Pan, Jean Karim Zinzindohoue
Implementing and Proving the TLS 1.3 Record Layer. IEEE Symposium on Security and Privacy (2017)
Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet
Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. EuroS&P (2017)
Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
. CoRR (2017)
Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
Verified low-level programming embedded in F. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Nadim Kobeissi
Formal Modeling and Verification for Domain Validation and ACME. Financial Cryptography (2017)
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay R. Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue
Everest: Towards a Verified, Drop-in Replacement of HTTPS. SNAPL (2017)
Karthikeyan Bhargavan, Ioana Boureanu, Pierre-Alain Fouque, Cristina Onete, Benjamin Richard
Content delivery over TLS: a cryptographic analysis of keyless SSL. EuroS&P (2017)
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
HACL*: A Verified Modern Cryptographic Library. CCS (2017)
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
HACL*: A Verified Modern Cryptographic Library. IACR Cryptol. ePrint Arch. 2017 (2017)
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
A messy state of the union: taming the composite state machines of TLS. Commun. ACM 60 (2) (2017)
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
Formal Verification of Smart Contracts: Short Paper. PLAS@CCS (2016)
Jean Karim Zinzindohoue, Evmorfia-Iro Bartzia, Karthikeyan Bhargavan
A Verified Extensible Library of Elliptic Curves. CSF (2016)
Karthikeyan Bhargavan, Gaëtan Leurent
Transcript Collision Attacks: Breaking Authentication in TLS, IKE and SSH. NDSS (2016)
Karthikeyan Bhargavan, Gaëtan Leurent
On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN. CCS (2016)
Karthikeyan Bhargavan, Gaëtan Leurent
On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN. IACR Cryptol. ePrint Arch. 2016 (2016)
Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella Béguelin
Downgrade Resilience in Key-Exchange Protocols. IEEE Symposium on Security and Privacy (2016)
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
Dependent types and multi-monadic effects in F. POPL (2016)
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss
miTLS: Verifying Protocol Implementations against Real-World Attacks. IEEE Secur. Priv. 14 (6) (2016)
Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella Béguelin
Downgrade Resilience in Key-Exchange Protocols. IACR Cryptol. ePrint Arch. 2016 (2016)
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
Implementing and Proving the TLS 1.3 Record Layer. IACR Cryptol. ePrint Arch. 2016 (2016)
David Adrian, Karthikeyan Bhargavan, Zakir Durumeric, Pierrick Gaudry, Matthew Green, J. Alex Halderman, Nadia Heninger, Drew Springall, Emmanuel Thomé, Luke Valenta, Benjamin VanderSloot, Eric Wustrow, Santiago Zanella Béguelin, Paul Zimmermann
Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice. CCS (2015)
Antoine Delignat-Lavaud, Karthikeyan Bhargavan
Network-based Origin Confusion Attacks against HTTPS Virtual Hosting. WWW (2015)
Benjamin Beurdouche, Antoine Delignat-Lavaud, Nadim Kobeissi, Alfredo Pironti, Karthikeyan Bhargavan
FLEXTLS: A Tool for Testing TLS Implementations. WOOT (2015)
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
A Messy State of the Union: Taming the Composite State Machines of TLS. IEEE Symposium on Security and Privacy (2015)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti, Adam Langley, Marsh Ray
Transport Layer Security (TLS) Session Hash and Extended Master Secret Extension. RFC 7627 (2015)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti
Verified Contributive Channel Bindings for Compound Authentication. NDSS (2015)
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin
Proving the TLS Handshake Secure (As It Is). CRYPTO (2) (2014)
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin
Proving the TLS Handshake Secure (as it is). IACR Cryptol. ePrint Arch. 2014 (2014)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. IEEE Symposium on Security and Privacy (2014)
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman
Gradual typing embedded securely in JavaScript. POPL (2014)
Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
Discovering concrete attacks on website authorization by formal analysis. J. Comput. Secur. 22 (4) (2014)
Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage. POST (2013)
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub
Implementing TLS with Verified Cryptographic Security. IEEE Symposium on Security and Privacy (2013)
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
Secure distributed programming with value-dependent types. J. Funct. Program. 23 (4) (2013)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
Defensive JavaScript - Building and Verifying Secure Web Components. FOSAD (2013)
Michael J. May, Karthikeyan Bhargavan
Towards Unified Authorization for Android. ESSoS (2013)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
Language-based Defenses Against Untrusted Browser Origins. USENIX Security Symposium (2013)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud
Web-based Attacks on Host-Proof Encrypted Storage. WOOT (2012)
Chetan Bansal, Karthikeyan Bhargavan, Sergio Maffeis
Discovering Concrete Attacks on Website Authorization by Formal Analysis. CSF (2012)
Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu
Verified Cryptographic Implementations for TLS. ACM Trans. Inf. Syst. Secur. 15 (1) (2012)
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
Secure distributed programming with value-dependent types. ICFP (2011)
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. 33 (2) (2011)
Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon
Cryptographic Verification by Typing for a Sample Protocol Implementation. FOSAD (2011)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
Modular verification of security protocol code by typing. POPL (2010)
Karthikeyan Bhargavan, Cédric Fournet, Nataliya Guts
Typechecking Higher-Order Security Libraries. APLAS (2010)
Johannes Borgström, Karthikeyan Bhargavan, Andrew D. Gordon
A compositional theory for STM Haskell. Haskell (2009)
Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, James J. Leifer
Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. CSF (2009)
Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer
A secure compiler for session abstractions. J. Comput. Secur. 16 (5) (2008)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
Verifying policy-based web services security. ACM Trans. Program. Lang. Syst. 30 (6) (2008)
Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu
Cryptographically verified implementations for TLS. CCS (2008)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse
Verified interoperable implementations of security protocols. ACM Trans. Program. Lang. Syst. 31 (1) (2008)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Nikhil Swamy
Verified implementations of the information card federated identity-management protocol. AsiaCCS (2008)
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
Refinement Types for Secure Implementations. CSF (2008)
Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya
Service Combinators for Farming Virtual Machines. COORDINATION (2008)
Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon
Secure sessions for Web services. ACM Trans. Inf. Syst. Secur. 10 (2) (2007)
Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya
Service Combinators for Farming Virtual Machines. TGC (2007)
Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer
Secure Implementations for Typed Session Abstractions. CSF (2007)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
Verified Reference Implementations of WS-Security Protocols. WS-FM (2006)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse
Verified Interoperable Implementations of Security Protocols. CSFW (2006)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
A semantics for web services authentication. Theor. Comput. Sci. 340 (1) (2005)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Greg O'Shea
An advisor for web services security policies. SWS (2005)
Karthikeyan Bhargavan, Carl A. Gunter
Network Event Recognition. Formal Methods Syst. Des. 27 (3) (2005)
Nishith Krishna, Marc Shapiro, Karthikeyan Bhargavan
Brief announcement: exploring the consistency problem space. PODC (2005)
Marc Shapiro, Karthikeyan Bhargavan, Nishith Krishna
A Constraint-Based Formalism for Consistency in Replicated Systems. OPODIS (2004)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
Verifying policy-based security for web services. CCS (2004)
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella
TulaFale: A Security Tool for Web Services CoRR (2004)

Karthikeyan Bhargavan.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Karthikeyan Bhargavan