Formal Analysis of Non-Malleability for Commitment Schemes in EasyCrypt
Name
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. Moreover, we validate our definition by proving that it implies hiding and binding of commitment schemes.
Graduation Thesis language
English
Graduation Thesis type
Master - Cyber Security
Supervisor(s)
Denis Firsov, Sven Laur
Defence year
2022