This repositiory contains the EasyCrypt formalisation of the paper:
- Formal security analysis of MPC-in-the-head zero-knowledge protocols. Nikolaj Sidorenco, Sabine Oechsner, and Bas Spitters. CSF 2021.
- Why3 1.3.3
- Z3 4.8.6
- Alt-Ergo 1.2.3
- Easycrypt Git hash ddb426b596c97417989ff28cf3f382649caee4af
- It is recommended to run
easycrypt why3configto set up the smt solvers.
- It is recommended to run
Defines the abstraction notion of a decompostion protocol and they security defintions.
Defines security of commitments schemes (With no secret keys)
Security definitions of Sigma-Protocols
General lemmas about foldr
An implementation of the ZKBoo MPC protocol, following the notion of decomposition protocols from Decomposition.eca.
A valid instance of a Sigma-Protocol, based on the ZKBoo Sigma-Protocol, showing security based on any decomposition satifying the security definitions.