UT Institute of Computer Science Graduation Theses Registry


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
PDF