The Crypto Proof Ladders project aims to provide a gentle introduction to formal methods for cryptography. The main idea is to present a collection of cryptographic problems with increasing levels of difficulty, formalized both as traditional pen-and-paper proofs and within different proof tools. The project is an initiative that originated from the HACS workshop and brings together cryptographers, cryptography engineers, and formal methods researchers. In this context, Paul Rösler and I contributed game-based definitions and proofs for unilateral authenticated key exchange protocols, available here. An EasyCrypt translation of the proof, mainly driven by François Dupressoir, is currently a work in progress.
Additional tools and resources are listed below.

The PELICAN project is an Équipe Associée with Inria, led by Sabrina Kunzweiler and myself. Funded by Inria, PELICAN focuses on the foundations of provable security for isogeny-based cryptographic protocols, and supports visits between our groups to foster closer collaboration.

I am part of the PQarrots submission to the NIST Threshold Cryptography Call. We propose post-quantum threshold primitives based on isogeny-based group actions, including threshold signatures, public-key encryption, and distributed key generation. A preview is available here. A more detailed version with full specifications, implementation details, and security proofs will follow.

I am generally interested in tools that support rigorous cryptographic proofs. While I am currently not involved in the development of such tools myself, I am actively supporting this area and am always happy to discuss ideas in this direction. Below are a few tools and resources developed by members of the community that I find particularly interesting:

• ProofFrog is a light-weight and easy-to-learn tool that checks game-hopping proof transitions in reduction-based security proofs.
• Domino is a tool to write and verify cryptographic proofs in the State-Separation Proofs framework. It can manage more tedious aspects, as they often come up in proofs for key exchange protocols.
• EasyCrypt is an interactive framework for machine-checked proofs of cryptographic schemes and protocols in the computational model. It is a very powerful tool, therefore not so easy to learn.

A direction that I find particularly interesting is how cryptographic proofs can be made more readable and interactive. Beyond traditional static LaTeX documents (who does ever read appendices), I believe that future proof presentations could allow structured navigation through games, reductions, and assumptions, making complex arguments easier to follow and verify. Related resources include:

• TeXFrog supports writing game-hopping proofs in LaTeX by automatically generating per-game renderings with highlighted differences.
• The Joy of Cryptography is a free undergraduate-level textbook by Mike Rosulek that introduces the fundamentals of provable security. The new web version is a nice example of presenting cryptographic content in a more structured and interactive way.

Lincoln Cryptools is a GitHub organization that hosts implementations of cryptographic schemes and tools, in particular for attribute-based encryption. The project includes code accompanying papers such as ABE Cubed and ISABELLA, to which I contributed on the theoretical aspects. Since then, my coauthors have continued to expand the project with new functionality and capabilities, which can be found on the organization's website.