Forking Lemma in EasyCrypt

Denis Firsov; Jakub Janků

Paper 2025/573

Forking Lemma in EasyCrypt

Denis Firsov

, Tallinn University of Technology, Input Output

Jakub Janků

, Masaryk University

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.
Keywords: computer-aided cryptography formal verification EasyCrypt rewinding forking Schnorr
Contact author(s): denis firsov @ taltech ee
jjanku @ mail muni cz
History: 2025-04-01: approved; 2025-03-29: received; See all versions
Short URL: https://ia.cr/2025/573
License: CC BY

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}
}