### Formal Analysis of Non-Malleability for Commitments in EasyCrypt

Denis Firsov, Sven Laur, and 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.

Available format(s)
Category
Foundations
Publication info
Preprint. MINOR revision.
Keywords
cryptographycommitmentsnon-malleabilityformal methodsEasyCrypt
Contact author(s)
denis firsov @ gmail com
History
Short URL
https://ia.cr/2022/032

CC BY

BibTeX

@misc{cryptoeprint:2022/032,
author = {Denis Firsov and Sven Laur and Ekaterina Zhuchko},
title = {Formal Analysis of Non-Malleability for Commitments in EasyCrypt},
howpublished = {Cryptology ePrint Archive, Paper 2022/032},
year = {2022},
note = {\url{https://eprint.iacr.org/2022/032}},
url = {https://eprint.iacr.org/2022/032}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.