Formalization of the Forking Lemma and Fiat-Shamir Transformation in EasyCrypt

See the eprint for more details about this project.

Setup

The project is checked using EasyCrypt 2025.03, see CI setup. Required SMT solvers can be found in easycrypt.project. (Other versions may work as well. Or not.)

More detailed installation instructions can be found on EasyCrypt's GitHub.

Verification

To check a single file, e.g., proof/Forking.ec, simply run:

easycrypt proof/Forking.ec

To check the whole project, use the following command:

easycrypt runtest tests.config proof

Note that this does not verify external dependencies (see deps); to do so, replace proof by deps in the above.