Charlie Jacomme

Full Time Researcher (CR) at Inria Nancy

Biography

Interests

Secure Messaging
Privacy
Formal Methods
Post-Quantum Security

Education

PhD in Computer Science, 2020

ENS Paris-Saclay

Awards

2 Distinguished paper awards at USENIX Security'23
PhD thesis Award of the GdR sécurité
PhD thesis Accessit of the Gilles Kahn award

Program committees

News

Signal

I did a formal analysis of Signal, which lead to several interesting findings and updates to the specification of the new PQXDH protocol. This is joint work with Cryspen and Signal, and this blog post details everything!

Signal

Videos

I’ve starting making some vulgarization videos. There’s a one-minute teaser preview for the Squirrel Prover, as well as a thirteen minutes video outlining its main concepts and ideas. And in French, my thesis in 137 seconds!

Videos

Squirrel Prover

One of my main projects is out in the wild. Learn more on the website now!

Squirrel Prover

Experience

Full time researcher (Chargé de Recherche)

Inria Nancy

Jan 2024 – Present Nancy

Full time researcher in the Pesto team.

Postdoc

Inria

Sep 2022 – Oct 2023 Paris

Postdoc in the Prosecco team with Bruno Blanchet.

Postdoc

CISPA

Nov 2020 – Jul 2022 Saarbrucken

Postdoc in the team of Cas Cremers.

PhD student

LSV, ENS Paris-Saclay

Sep 2017 – Sep 2020

PhD under the supervision of Hubert Comon and Steve Kremer.

Recent Posts

Notes from a 10 days Workshop with Keith Johnstone

I have been doing some improvisation theatre for half of a decade now. In October 2018, I had the opportinity to participate in a 10 days Workshop with Keith Johnstone, one of the pioneers of improvisation.

Last updated on Apr 30, 2021

Notes from a 10 days Workshop with Keith Johnstone

Recent Publications

Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt (2024). Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. USENIX Security Symposium (USENIX Security), 2024.

Bruno Blanchet, Charlie Jacomme (2024). Post-quantum sound CryptoVerif and verification of hybrid TLS and SSH key-exchanges. Proceedings of the 37th IEEE Computer Security Foundations Symposium (CSF'24).

Charlie Jacomme, Elise Klein, Steve Kremer, Maïwenn Racouchot (2023). A comprehensive, formal and automated analysis of the EDHOC protocol. USENIX Security Symposium (USENIX Security), 2023.

Cas Cremers, Alexander Dax, Charlie Jacomme, Mang Zhao (2023). Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security. USENIX Security Symposium (USENIX Security), 2023.
🏆 Distinguished Paper Award.

Cas Cremers, Charlie Jacomme, Aurora Naska (2023). Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations. USENIX Security Symposium (USENIX Security), 2023.

See all publications

Recent & Upcoming Talks

A formal composition framework

A composition framework suitable for the Bana-Comon logic.

Jan 29, 2020 At CISPA and TU Wien

Decisions problems about propabilistic programs over finite fields, decidability and complexity.

Sep 26, 2019 LICS'20, Annual PhD students day of the formal methods department of LORIA

Symbolic methods in computational cryptography proofs

Jun 18, 2019 CSF'19, Journée GT MFS 2019 and Pesto working group

Gröbner Basis and deducibility

Oct 26, 2018 EJCIM 2018 spring school

Symbolic methods applied to the automation of computational proofs - Building simulators

Aug 12, 2018 FOSAD 18 summer school and Annual PhD students day of the formal methods department of LORIA