Internships/PhDs

For each of my topics (see below for details, but here’s a first quick keyword list: Formal Methods, Cryptography, Logic, Security Protocol, Privacy, Post-Quantum, OCaml), tailored master internship or PhD projects can be designed, depending on your desires and preferences, notably with a range of more theoretical/applied projects.

If you are interested, just contact me at charlie.jacomme@inria.fr with a brief description of yourself and we’ll set up an online meeting.

Soon to be opened: postdocs/engineers

I will receive funding in the nearish future (final administrative process in progress…) for post-doc and engineers position, with a focus on the post-quantum part of the project. Detailed proposal will be published once the funding is officially in, but you can already contact me

Research topics and me

I’m Charlie (he/him), a youngish (born in 1994) full-time researcher at Inria Nancy in the PESTO team.

My main research goal is to obtain formal guarantees over the security and privacy provided by security protocols (SSH, TLS/HTTPs, Signal,…). I develop, participate in and use several provers (computer programs that do, check or help us do security proofs), and I like to question the gaps between our formal models or proofs and the real-world. On the practical side, I am particularly interested in open-source applications that aim at improving the privacy of citizens, such as secure messaging applications (Signal, Matrix,…) and VPNs.

In a bit more details, my main working topics are:

• development of the Squirrel Prover (interactive prover for security protocols in higher-order logic, OCaml programing)
• development of CryptoVerif (cryptographic game hops, OCaml programing)
• proofs of security protocol (my current preference is on messaging protocols such as Signal/Matrix/… or privacy preserving projects such as WireGuard), using Squirrel/CryptoVerif/ProVerif/Tamarin/Sapic/…
• foundational aspects of security protocols verification (developing practical composition results, gaps between our formal models/security definitions and the real-world, …)
• the transition to post-quantum secure protocols, for instance looking at the current development of hybride key-exchanges, e.g., RosenPass.

I welcome applications from anyone from anywhere, up to several important points:

• The academic world inherits from the many systemic inequalities of our societies, and as such, people from minorities and discriminated groups often statistically have a harder time in research. I cannot solve systemic problems, but I consider it one of my duties to build a safe and inclusive working place, and try to do my best for this. I shall always be open to criticisms on my behavior.
• Academical excellency is not required, as grades often do not reflect the capacity to do research.
• Being open-minded and respectful are required. Notably, I do not tolerate intolerance, and I will not be able to collaborate with anybody showing signs of racism, sexism, transphobia, islamophobia, antisemitism, LGBTQIA+phobia, classism, ableism, … (generally any kind of discriminatory behavior). I will also not be able to collaborate with people supporting acts such as wars, terrorism, colonisations, or genocides such as the ongoing palestinian genocide by the state of Israel.
• For ecological reasons, I do not take the plane to travel. In addition, I would ideally only target conferences with open access publications. I will however compromise on this, as I want to do my utmost to give the desired career opportunities to students, and will thus also try to target conferences following the interests of students.

As a final note, the picture on my homepage is deceiving: as per tradition, it is nicely outdated from around 2018, the main difference is that I am now frequently bald.

Concrete proposals

Here are a couple of concrete proposals, but this is only a subset of what may be done, as said, I am happy to discuss and come up with a tailored made project.

• Internship proposal for cryptographic proof of Signal Messenger that takes into account key reuse, using CryptoVerif (cryptographic proofs).
• Internship proposal for formalizing in its theory the support of multi-term in the Squirrel Prover (higher-order logic, interactive prover, OCaml implementation).
• (past offer already taken) Internship proposal for integrating a composition result inside the theory of the Squirrel Prover.

Past supervisions

It is always recomended to ask people what they think of your potential supervisor. Feel free to contact people I have worked with and supervised in the past if you want opinions!

• Aurora Naska (2022-2023, PhD student of Cas Cremers, part-time supervised during a post-doc)
• Alexander Dax (2022-2023, PhD student of Cas Cremers, part-time supervised during a post-doc)
• Philip Lukert (2021-2022, PhD student of Cas Cremers, part-time supervised during a post-doc)

Final tip: if you have read everything until there, you should include the word petrichore in your email!