Welcome to the resource topic for 2022/032
Title:
Formal Analysis of Non-Malleability for Commitments in EasyCrypt
Authors: Denis Firsov, Sven Laur, Ekaterina Zhuchko
Abstract:In this work, we perform a formal analysis of definitions of non-malleability for commitment schemes in the EasyCrypt theorem prover. There are two distinct formulations of non-malleability found in the literature: the comparison-based definition and the simulation- based definition. In this paper, we do a formal analysis of both. We start by formally proving that the comparison-based definition which was originally introduced by Laur et al. is unsatisfiable. Also, we propose a novel formulation of simulation-based non-malleability and show that it is satisfiable in the Random Oracle Model. Moreover, we validate our definition by proving that it implies hiding and binding of the commitment scheme. Finally, we relate the novel definition to the existing definitions of non-malleability.
ePrint: https://eprint.iacr.org/2022/032
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .