Karthikeyan Bhargavan

Orcid: 0000-0002-3152-8997

Affiliations:
  • INRIA, France


According to our database1, Karthikeyan Bhargavan authored at least 91 papers between 1998 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
KyberSlash: Exploiting secret-dependent division timings in Kyber implementations.
IACR Cryptol. ePrint Arch., 2024

Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging.
Proceedings of the 33rd USENIX Security Symposium, 2024

2023
Foundations of WebAssembly (Dagstuhl Seminar 23101).
Dagstuhl Reports, March, 2023

Comparse: Provably Secure Formats for Cryptographic Protocols.
IACR Cryptol. ePrint Arch., 2023

Layered Symbolic Security Analysis in DY$^\star$.
IACR Cryptol. ePrint Arch., 2023

From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake.
Proceedings of the 8th IEEE European Symposium on Security and Privacy, 2023

Layered Symbolic Security Analysis in $\textsf {DY}^\star $.
Proceedings of the Computer Security - ESORICS 2023, 2023

2022
Hybrid Public Key Encryption.
RFC, February, 2022

TreeSync: Authenticated Group Management for Messaging Layer Security.
IACR Cryptol. ePrint Arch., 2022

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version).
IACR Cryptol. ePrint Arch., 2022

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations.
Proceedings of the 43rd IEEE Symposium on Security and Privacy, 2022

A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello.
Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, 2022

2021
An In-Depth Symbolic Security Analysis of the ACME Standard.
IACR Cryptol. ePrint Arch., 2021

DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code.
Proceedings of the IEEE European Symposium on Security and Privacy, 2021

A Tutorial-Style Introduction to DY*.
Proceedings of the Protocols, Strands, and Logic, 2021

2020
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms).
IACR Cryptol. ePrint Arch., 2020


HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms).
Proceedings of the CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020

2019
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch., 2019

Formally Verified Cryptographic Web Applications in WebAssembly.
IACR Cryptol. ePrint Arch., 2019

SoK: Computer-Aided Cryptography.
IACR Cryptol. ePrint Arch., 2019

Imperfect forward secrecy: how Diffie-Hellman fails in practice.
Commun. ACM, 2019

Practical Formal Methods for Real World Cryptography (Invited Talk).
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.
Proceedings of the IEEE European Symposium on Security and Privacy, 2019

Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols.
Proceedings of the IEEE European Symposium on Security and Privacy, 2019

2018
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols.
IACR Cryptol. ePrint Arch., 2018

A Formal Treatment of Accountable Proxying Over TLS.
Proceedings of the 2018 IEEE Symposium on Security and Privacy, 2018

hacspec: Towards Verifiable Crypto Standards.
Proceedings of the Security Standardisation Research - 4th International Conference, 2018

2017
Verified low-level programming embedded in F.
Proc. ACM Program. Lang., 2017

HACL*: A Verified Modern Cryptographic Library.
IACR Cryptol. ePrint Arch., 2017

Verified Low-Level Programming Embedded in F<sup>*</sup>.
CoRR, 2017

A messy state of the union: taming the composite state machines of TLS.
Commun. ACM, 2017

Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate.
Proceedings of the 2017 IEEE Symposium on Security and Privacy, 2017


Formal Modeling and Verification for Domain Validation and ACME.
Proceedings of the Financial Cryptography and Data Security, 2017

Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach.
Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

Content delivery over TLS: a cryptographic analysis of keyless SSL.
Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

2016
miTLS: Verifying Protocol Implementations against Real-World Attacks.
IEEE Secur. Priv., 2016

On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN.
IACR Cryptol. ePrint Arch., 2016

Implementing and Proving the TLS 1.3 Record Layer.
IACR Cryptol. ePrint Arch., 2016

Downgrade Resilience in Key-Exchange Protocols.
IACR Cryptol. ePrint Arch., 2016

Dependent types and multi-monadic effects in F.
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.
Proceedings of the 23rd Annual Network and Distributed System Security Symposium, 2016

A Verified Extensible Library of Elliptic Curves.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

Formal Verification of Smart Contracts: Short Paper.
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.
RFC, September, 2015

Network-based Origin Confusion Attacks against HTTPS Virtual Hosting.
Proceedings of the 24th International Conference on World Wide Web, 2015

FLEXTLS: A Tool for Testing TLS Implementations.
Proceedings of the 9th USENIX Workshop on Offensive Technologies, 2015

Verified Contributive Channel Bindings for Compound Authentication.
Proceedings of the 22nd Annual Network and Distributed System Security Symposium, 2015

2014
Discovering concrete attacks on website authorization by formal analysis.
J. Comput. Secur., 2014

Proving the TLS Handshake Secure (as it is).
IACR Cryptol. ePrint Arch., 2014

Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS.
Proceedings of the 2014 IEEE Symposium on Security and Privacy, 2014

Gradual typing embedded securely in JavaScript.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013
Secure distributed programming with value-dependent types.
J. Funct. Program., 2013

Language-based Defenses Against Untrusted Browser Origins.
Proceedings of the 22th USENIX Security Symposium, Washington, DC, USA, August 14-16, 2013, 2013

Implementing TLS with Verified Cryptographic Security.
Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage.
Proceedings of the Principles of Security and Trust - Second International Conference, 2013

Defensive JavaScript - Building and Verifying Secure Web Components.
Proceedings of the Foundations of Security Analysis and Design VII, 2013

Towards Unified Authorization for Android.
Proceedings of the Engineering Secure Software and Systems - 5th International Symposium, 2013

2012
Verified Cryptographic Implementations for TLS.
ACM Trans. Inf. Syst. Secur., 2012

Web-based Attacks on Host-Proof Encrypted Storage.
Proceedings of the 6th USENIX Workshop on Offensive Technologies, 2012

Discovering Concrete Attacks on Website Authorization by Formal Analysis.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

2011
Refinement types for secure implementations.
ACM Trans. Program. Lang. Syst., 2011

Cryptographic Verification by Typing for a Sample Protocol Implementation.
Proceedings of the Foundations of Security Analysis and Design VI, 2011

2010
Modular verification of security protocol code by typing.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Typechecking Higher-Order Security Libraries.
Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009
A compositional theory for STM Haskell.
Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, 2009

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions.
Proceedings of the 22nd IEEE Computer Security Foundations Symposium, 2009

2008
Verified interoperable implementations of security protocols.
ACM Trans. Program. Lang. Syst., 2008

Verifying policy-based web services security.
ACM Trans. Program. Lang. Syst., 2008

A secure compiler for session abstractions.
J. Comput. Secur., 2008

Verified implementations of the information card federated identity-management protocol.
Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, 2008

Cryptographically verified implementations for TLS.
Proceedings of the 2008 ACM Conference on Computer and Communications Security, 2008

2007
Secure sessions for Web services.
ACM Trans. Inf. Syst. Secur., 2007

Service Combinators for Farming Virtual Machines.
Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

Secure Implementations for Typed Session Abstractions.
Proceedings of the 20th IEEE Computer Security Foundations Symposium, 2007

2006
Verified Reference Implementations of WS-Security Protocols.
Proceedings of the Web Services and Formal Methods, Third International Workshop, 2006

2005
A semantics for web services authentication.
Theor. Comput. Sci., 2005

Network Event Recognition.
Formal Methods Syst. Des., 2005

An advisor for web services security policies.
Proceedings of the 2nd ACM Workshop On Secure Web Services, 2005

Brief announcement: exploring the consistency problem space.
Proceedings of the Twenty-Fourth Annual ACM Symposium on Principles of Distributed Computing, 2005

2004
A Constraint-Based Formalism for Consistency in Replicated Systems.
Proceedings of the Principles of Distributed Systems, 8th International Conference, 2004

Verifying policy-based security for web services.
Proceedings of the 11th ACM Conference on Computer and Communications Security, 2004

2003
TulaFale: A Security Tool for Web Services.
Proceedings of the Formal Methods for Components and Objects, 2003

2002
Verisim: Formal Analysis of Network Simulations.
IEEE Trans. Software Eng., 2002

Formal verification of standards for distance vector routing protocols.
J. ACM, 2002

Requirements for a Practical Network Event Recognition Language.
Proceedings of the Runtime Verification 2002, 2002

2001
What packets may come: automata for network monitoring.
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.
Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Fault origin adjudication.
Proceedings of the Third Workshop on Formal Methods in Software Practice, 2000

1998
The Village Telephone System: A Case Study in Formal Software Engineering.
Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998


  Loading...