Forking Lemma in EasyCrypt

Denis Firsov; Jakub Janků

Paper 2025/573 Original: eprint.iacr.org/2025/573 ↗

Forking Lemma in EasyCrypt

Denis Firsov

Jakub Janků

Abstract

Formal methods are becoming an important tool for ensuring correctness and security of cryptographic constructions. However, the support for certain advanced proof techniques, namely rewinding, is scarce among existing verification frameworks, which hinders their application to complex schemes such as multi-party signatures and zero-knowledge proofs. We expand the support for rewinding in EasyCrypt by implementing a version of the general forking lemma by Bellare and Neven. We demonstrate its usability by proving EUF-CMA security of Schnorr signatures.

Metadata

Available format(s): PDF
Category: Foundations
Publication info: Preprint.
History: 2026-02-17: last updated; 2025-03-29: published
Short URL: https://ia.cr/2025/573
License: https://creativecommons.org/licenses/by/4.0/

BibTeX

@misc{cryptoeprint:2025/573,
      author = {Denis Firsov and Jakub Janků},
      title = {Forking Lemma in EasyCrypt},
      howpublished = {Cryptology {ePrint} Archive, Paper 2025/573},
      year = {2025},
      url = {https://eprint.iacr.org/2025/573}
}