Charlie Jacomme

PostDoc at CISPA

Biography

Interests

Protocol Security
Privacy
Formal Methods
Composition Frameworks

Education

PhD in Computer Science, 2020
ENS Paris-Saclay

News

PhD Thesis Award

I got the PhD thesis Award of the GdR sécurité as well as an accessit for the Gilles Kahn award. Thanks to the jurees!

PhD Thesis Award

NoLimitSecu Podcast

I have been invited by the (french) podcast NoLimitSecu , dedicated to cybersecurity. The episode can be found here. They have lots of interesting stuff (in french), check it out!

NoLimitSecu Podcast

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

CSF'22 Program committee

Just joined the CSF'22 PC, and hoping to read your best papers!

CSF'22 Program committee

Squirrel Prover

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

Squirrel Prover

Experience

Postdoc

CISPA

Nov 2020 – Present 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 Publications

Cas Cremers, Caroline Fontaine, Charlie Jacomme (2022). A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols (to appear). Proceedings of the 43nd IEEE Symposium on Security and Privacy (S&P'22) - To appear.

Gilles Barthe, Charlie Jacomme, Steve Kremer (2021). Universal Equivalence and Majority of Probabilistic Programs over Finite Fields. ACM Trans. Comput. Logic.

Charlie Jacomme, Steve Kremer (2021). An extensive formal analysis of multi-factor authentication protocols. ACM Transactions on Privacy and Security (TOPS).

David Baelde, Stéphanie Delaune, Adrien Koutsos, Charlie Jacomme, Solène Moreau (2021). An interactive prover for protocol verification in the computational model. IEEE Symposium on Security and Privacy (S&P'21).

Hubert Comon, Charlie Jacomme, Guillaume Scerri (2020). Oracle simulation: a technique for protocol composition with long term shared secrets. Proceedings of the 27st ACM Conference on Computer and Communications Security (CCS'20).

PDF Long Version

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