**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

We use CryptHOL to formalise commitment schemes and Sigma-protocols.
Both are widely used fundamental two party cryptographic primitives.
Security for commitment schemes is considered using game-based
definitions whereas the security of Sigma-protocols is considered
using both the game-based and simulation-based security paradigms. In
this work, we first define security for both primitives and then prove
secure multiple case studies: the Schnorr, Chaum-Pedersen and
Okamoto Sigma-protocols as well as a construction that allows for
compound (AND and OR statements) Sigma-protocols and the Pedersen and
Rivest commitment schemes. We also prove that commitment schemes can
be constructed from Sigma-protocols. We formalise this proof at an
abstract level, only assuming the existence of a Sigma-protocol;
consequently, the instantiations of this result for the concrete
Sigma-protocols we consider come for free.

### License

### Topics

### Session Sigma_Commit_Crypto

- Commitment_Schemes
- Cyclic_Group_Ext
- Discrete_Log
- Number_Theory_Aux
- Uniform_Sampling
- Pedersen
- Rivest
- Sigma_Protocols
- Schnorr_Sigma_Commit
- Chaum_Pedersen_Sigma_Commit
- Okamoto_Sigma_Commit
- Xor
- Sigma_AND
- Sigma_OR