Abstract
There are two distinct formulations of non-malleability of commitments found in the literature: the comparison-based definition and the simulation-based definition. In this paper, we prove that the comparison-based definition is unstatisfiable by any realistic commitment scheme. Our proof is fully formalized in the EasyCrypt theorem prover.
[pdf, github, MSc thesis of E. Zhuchko, slides from ICTAC'22]