Year

Venue

Title

2025

journals/tches

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

2025

conf/sp

TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security.

Théophile Wallez Jonathan Protzenko Karthikeyan Bhargavan

2024

conf/uss

Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging.

Karthikeyan Bhargavan Charlie Jacomme Franziskus Kiefer Rolfe Schmidt

2023

conf/ccs

Comparse: Provably Secure Formats for Cryptographic Protocols.

Théophile Wallez Jonathan Protzenko Karthikeyan Bhargavan

2023

conf/uss

TreeSync: Authenticated Group Management for Messaging Layer Security.

Théophile Wallez Jonathan Protzenko Benjamin Beurdouche Karthikeyan Bhargavan

2023

conf/eurosp

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

2023

conf/esorics

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

2022

conf/ccs

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

Karthikeyan Bhargavan Vincent Cheval Christopher A. Wood

2022

conf/sp

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

Son Ho Jonathan Protzenko Abhishek Bichhawat Karthikeyan Bhargavan

2021

conf/ccs

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

2021

conf/eurosp

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

2020

conf/ccs

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

2020

conf/sp

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

2019

conf/sp

Formally Verified Cryptographic Web Applications in WebAssembly.

Jonathan Protzenko Benjamin Beurdouche Denis Merigoux Karthikeyan Bhargavan

2019

conf/eurosp

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

Benjamin Lipp Bruno Blanchet Karthikeyan Bhargavan

2019

conf/eurosp

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

Nadim Kobeissi Georgio Nicolas Karthikeyan Bhargavan

2018

conf/sp

A Formal Treatment of Accountable Proxying Over TLS.

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

2017

conf/ccs

HACL*: A Verified Modern Cryptographic Library.

Jean Karim Zinzindohoué Karthikeyan Bhargavan Jonathan Protzenko Benjamin Beurdouche

2017

conf/fc

Formal Modeling and Verification for Domain Validation and ACME.

Karthikeyan Bhargavan Antoine Delignat-Lavaud Nadim Kobeissi

2017

conf/sp

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

Karthikeyan Bhargavan Bruno Blanchet Nadim Kobeissi

2017

conf/sp

Implementing and Proving the TLS 1.3 Record Layer.

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

2017

conf/eurosp

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

Nadim Kobeissi Karthikeyan Bhargavan Bruno Blanchet

2017

conf/eurosp

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

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

2016

conf/ccs

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

2016

conf/ccs

On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN.

Karthikeyan Bhargavan Gaëtan Leurent

2016

conf/sp

Downgrade Resilience in Key-Exchange Protocols.

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

2016

conf/ndss

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

Karthikeyan Bhargavan Gaëtan Leurent

2015

conf/ccs

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

2015

conf/sp

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

2015

conf/ndss

Verified Contributive Channel Bindings for Compound Authentication.

Karthikeyan Bhargavan Antoine Delignat-Lavaud Alfredo Pironti

2014

conf/crypto

Proving the TLS Handshake Secure (As It Is).

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

2014

conf/sp

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

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