Paper 2022/032
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.
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- Preprint. MINOR revision.
- Keywords
- cryptographycommitmentsnon-malleabilityformal methodsEasyCrypt
- Contact author(s)
- denis firsov @ gmail com
- History
- 2022-01-14: received
- Short URL
- https://ia.cr/2022/032
- License
-
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}
}
