Security arguments for many modern cryptographic schemes rely on rewinding. However, formal verification of these proofs remains challenging due to limited support for this technique even in specialized tools such as EasyCrypt, an interactive proof assistant tailored for cryptography.

The aim of the thesis is to formalize the forking lemma, a special case of rewinding, in EasyCrypt and thereby broaden the class of security proofs that can be mechanized using this toolset.

Specifically, the student will:

• become proficient with EasyCrypt,
• study the rewinding technique and the forking lemma [1],
• survey prior formalizations of rewinding in EasyCrypt [2] and, if relevant, in other tools;
• propose a formal model for forkable adversaries,
• formalize (a variant of) the forking lemma in EasyCrypt, and
• apply it in a non-trivial setting (e.g., establish existential unforgeability of Schnorr signatures).

Technical work on the thesis research will be lead by a co-supervisor - Denis Firsov, PhD, Tallinn University of Technology, Department of Software Science - and supported by the CHESS (Cyber-security Excellence Hub in Estonia and South Moravia) project.

Literature:
[1] Mihir Bellare and Gregory Neven. “Multi-Signatures in the Plain Public-Key Model and a General Forking Lemma”,
[2] Denis Firsov and Dominique Unruh. “Reflection, Rewinding, and Coin-Toss in EasyCrypt”.