Formal Analysis of Non-Malleability for Commitments in EasyCrypt
| Main Author: | Anonymous |
|---|---|
| Format: | info software Journal |
| Terbitan: |
, 2022
|
| Online Access: |
https://zenodo.org/record/6382539 |
Daftar Isi:
- 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.