This work is known to work with EasyCrypt built from GIT hash: 132968e41afcc3a9834a9f12d19cbcbae0546535

The code can be found in the "code/" subfolder.

Contains an abstract specification of Sigma Protocols and their security definitions. Also contains a proof Fiat-Shamir.

Contains an abstract specification of Commitment Schemes and their security definitions.

Abstract specification of key-less commitment schemes

Formalisation of the Pedersen Commitment Scheme

Formalisation of Schnorr's protocols.

Proof of the AND compound Sigma-protocol.

Proof of the OR compound Sigma-protocol.

Formalisation of arithmetic circuits and the (2,3)-Decomposition.

Formalisation of the ZKBoo protocol. Depends on SigmaProtocols.eca, IdealCommitment.ec, and Decompose.ec