Karthikeyan Bhargavan

According to our database, Karthikeyan Bhargavan authored at least 89 papers between 1998 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

Foundations of WebAssembly (Dagstuhl Seminar 23101).

Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, Deian Stefan

Dagstuhl Reports, March, 2023

Comparse: Provably Secure Formats for Cryptographic Protocols.

Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan

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

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

Proceedings of the 8th IEEE European Symposium on Security and Privacy, 2023

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

Proceedings of the Computer Security - ESORICS 2023, 2023

2022

Hybrid Public Key Encryption.

Richard L. Barnes, Karthikeyan Bhargavan, Benjamin Lipp, Christopher A. Wood

RFC, February, 2022

TreeSync: Authenticated Group Management for Messaging Layer Security.

Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan

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

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations.

Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan

Proceedings of the 43rd IEEE Symposium on Security and Privacy, 2022

A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello.

Karthikeyan Bhargavan, Vincent Cheval, Christopher A. Wood

Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, 2022

2021

An In-Depth Symbolic Security Analysis of the ACME Standard.

Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele

IACR Cryptol. ePrint Arch., 2021

DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code.

Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele

Proceedings of the IEEE European Symposium on Security and Privacy, 2021

A Tutorial-Style Introduction to DY*.

Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele

Proceedings of the Protocols, Strands, and Logic, 2021

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

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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

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

Proceedings of the CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020

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, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin

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

SoK: Computer-Aided Cryptography.

Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno

IACR Cryptol. ePrint Arch., 2019

Imperfect forward secrecy: how Diffie-Hellman fails in practice.

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

Commun. ACM, 2019

Practical Formal Methods for Real World Cryptography (Invited Talk).

Karthikeyan Bhargavan, Prasad Naldurg

Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2019

A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol.

Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan

Proceedings of the IEEE European Symposium on Security and Privacy, 2019

Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols.

Nadim Kobeissi, Georgio Nicolas, Karthikeyan Bhargavan

Proceedings of the IEEE European Symposium on Security and Privacy, 2019

2018

Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols.

Nadim Kobeissi, Karthikeyan Bhargavan

IACR Cryptol. ePrint Arch., 2018

A Formal Treatment of Accountable Proxying Over TLS.

Karthikeyan Bhargavan, Ioana Boureanu, Antoine Delignat-Lavaud, Pierre-Alain Fouque, Cristina Onete

Proceedings of the 2018 IEEE Symposium on Security and Privacy, 2018

hacspec: Towards Verifiable Crypto Standards.

Karthikeyan Bhargavan, Franziskus Kiefer, Pierre-Yves Strub

Proceedings of the Security Standardisation Research - 4th International Conference, 2018

2017

Verified low-level programming embedded in F.

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

Proc. ACM Program. Lang., 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, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy

CoRR, 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, Pierre-Yves Strub, Jean Karim Zinzindohoue

Commun. ACM, 2017

Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate.

Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi

Proceedings of the 2017 IEEE Symposium on Security and Privacy, 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, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

Formal Modeling and Verification for Domain Validation and ACME.

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Nadim Kobeissi

Proceedings of the Financial Cryptography and Data Security, 2017

Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach.

Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet

Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

Content delivery over TLS: a cryptographic analysis of keyless SSL.

Karthikeyan Bhargavan, Ioana Boureanu, Pierre-Alain Fouque, Cristina Onete, Benjamin Richard

Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

2016

miTLS: Verifying Protocol Implementations against Real-World Attacks.

Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss

IEEE Secur. Priv., 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

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

Downgrade Resilience in Key-Exchange Protocols.

Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella Béguelin

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

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Transcript Collision Attacks: Breaking Authentication in TLS, IKE and SSH.

Karthikeyan Bhargavan, Gaëtan Leurent

Proceedings of the 23rd Annual Network and Distributed System Security Symposium, 2016

A Verified Extensible Library of Elliptic Curves.

Jean Karim Zinzindohoue, Evmorfia-Iro Bartzia, Karthikeyan Bhargavan

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

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

Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, 2016

2015

Transport Layer Security (TLS) Session Hash and Extended Master Secret Extension.

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti, Adam Langley, Marsh Ray

RFC, September, 2015

Network-based Origin Confusion Attacks against HTTPS Virtual Hosting.

Antoine Delignat-Lavaud, Karthikeyan Bhargavan

Proceedings of the 24th International Conference on World Wide Web, 2015

FLEXTLS: A Tool for Testing TLS Implementations.

Benjamin Beurdouche, Antoine Delignat-Lavaud, Nadim Kobeissi, Alfredo Pironti, Karthikeyan Bhargavan

Proceedings of the 9th USENIX Workshop on Offensive Technologies, 2015

Verified Contributive Channel Bindings for Compound Authentication.

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti

Proceedings of the 22nd Annual Network and Distributed System Security Symposium, 2015

2014

Discovering concrete attacks on website authorization by formal analysis.

Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis

J. Comput. Secur., 2014

Proving the TLS Handshake Secure (as it is).

Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin

IACR Cryptol. ePrint Arch., 2014

Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS.

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub

Proceedings of the 2014 IEEE Symposium on Security and Privacy, 2014

Gradual typing embedded securely in JavaScript.

Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013

Secure distributed programming with value-dependent types.

Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang

J. Funct. Program., 2013

Language-based Defenses Against Untrusted Browser Origins.

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis

Proceedings of the 22th USENIX Security Symposium, Washington, DC, USA, August 14-16, 2013, 2013

Implementing TLS with Verified Cryptographic Security.

Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub

Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage.

Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis

Proceedings of the Principles of Security and Trust - Second International Conference, 2013

Defensive JavaScript - Building and Verifying Secure Web Components.

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis

Proceedings of the Foundations of Security Analysis and Design VII, 2013

Towards Unified Authorization for Android.

Michael J. May, Karthikeyan Bhargavan

Proceedings of the Engineering Secure Software and Systems - 5th International Symposium, 2013

2012

Verified Cryptographic Implementations for TLS.

Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu

ACM Trans. Inf. Syst. Secur., 2012

Web-based Attacks on Host-Proof Encrypted Storage.

Karthikeyan Bhargavan, Antoine Delignat-Lavaud

Proceedings of the 6th USENIX Workshop on Offensive Technologies, 2012

Discovering Concrete Attacks on Website Authorization by Formal Analysis.

Chetan Bansal, Karthikeyan Bhargavan, Sergio Maffeis

Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

2011

Refinement types for secure implementations.

Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis

ACM Trans. Program. Lang. Syst., 2011

Cryptographic Verification by Typing for a Sample Protocol Implementation.

Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon

Proceedings of the Foundations of Security Analysis and Design VI, 2011

2010

Modular verification of security protocol code by typing.

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Typechecking Higher-Order Security Libraries.

Karthikeyan Bhargavan, Cédric Fournet, Nataliya Guts

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

A compositional theory for STM Haskell.

Johannes Borgström, Karthikeyan Bhargavan, Andrew D. Gordon

Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, 2009

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions.

Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, James J. Leifer

Proceedings of the 22nd IEEE Computer Security Foundations Symposium, 2009

2008

Verified interoperable implementations of security protocols.

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse

ACM Trans. Program. Lang. Syst., 2008

Verifying policy-based web services security.

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon

ACM Trans. Program. Lang. Syst., 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

Verified implementations of the information card federated identity-management protocol.

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Nikhil Swamy

Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, 2008

Cryptographically verified implementations for TLS.

Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu

Proceedings of the 2008 ACM Conference on Computer and Communications Security, 2008

2007

Secure sessions for Web services.

Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon

ACM Trans. Inf. Syst. Secur., 2007

Service Combinators for Farming Virtual Machines.

Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya

Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

Secure Implementations for Typed Session Abstractions.

Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer

Proceedings of the 20th IEEE Computer Security Foundations Symposium, 2007

2006

Verified Reference Implementations of WS-Security Protocols.

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon

Proceedings of the Web Services and Formal Methods, Third International Workshop, 2006

2005

A semantics for web services authentication.

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon

Theor. Comput. Sci., 2005

Network Event Recognition.

Karthikeyan Bhargavan, Carl A. Gunter

Formal Methods Syst. Des., 2005

An advisor for web services security policies.

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Greg O'Shea

Proceedings of the 2nd ACM Workshop On Secure Web Services, 2005

Brief announcement: exploring the consistency problem space.

Nishith Krishna, Marc Shapiro, Karthikeyan Bhargavan

Proceedings of the Twenty-Fourth Annual ACM Symposium on Principles of Distributed Computing, 2005

2004

A Constraint-Based Formalism for Consistency in Replicated Systems.

Marc Shapiro, Karthikeyan Bhargavan, Nishith Krishna

Proceedings of the Principles of Distributed Systems, 8th International Conference, 2004

Verifying policy-based security for web services.

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon

Proceedings of the 11th ACM Conference on Computer and Communications Security, 2004

2003

TulaFale: A Security Tool for Web Services.

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella

Proceedings of the Formal Methods for Components and Objects, 2003

2002

Verisim: Formal Analysis of Network Simulations.

Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, Mahesh Viswanathan

IEEE Trans. Software Eng., 2002

Formal verification of standards for distance vector routing protocols.

Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gunter

J. ACM, 2002

Requirements for a Practical Network Event Recognition Language.

Karthikeyan Bhargavan, Carl A. Gunter

Proceedings of the Runtime Verification 2002, 2002

2001

What packets may come: automata for network monitoring.

Karthikeyan Bhargavan, Satish Chandra, Peter J. McCann, Carl A. Gunter

Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001

2000

Routing Information Protocol in HOL/SPIN.

Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Fault origin adjudication.

Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic

Proceedings of the Third Workshop on Formal Methods in Software Practice, 2000

1998

The Village Telephone System: A Case Study in Formal Software Engineering.

Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave

Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998