Paper 2019/1185 Original: eprint.iacr.org/2019/1185 ↗
Formalising $\Sigma$-Protocols and Commitment Schemes using CryptHOL
Abstract
Machine-checked proofs of security are important to increase the rigour of provable security. In this work we present a formalised theory of two fundamental two party cryptographic primitives: $\Sigma$-protocols and Commitment Schemes. $\Sigma$-protocols allow a prover to convince a verifier that they possess some knowledge without leaking information about the knowledge. Commitment schemes allow a committer to commit to a message and keep it secret until revealing it at a later time. We use CryptHOL to formalise both primitives and prove secure multiple examples namely; the Schnorr, Chaum-Pedersen and Okamoto $\Sigma$-protocols as well as a construction that allows for compound (AND and OR) $\Sigma$-protocols and the Pedersen and Rivest commitment schemes. A highlight of the work is a formalisation of the construction of commitment schemes from $\Sigma$-protocols. We formalise this proof at an abstract level using the modularity available in Isabelle/HOL and CryptHOL. This way, the proofs of the instantiations come for free.
Metadata
- Available format(s)
PDF- Category
- Foundations
- Publication info
- Preprint.
- History
- 2019-10-15: last updated
- 2019-10-15: published
- Short URL
- https://ia.cr/2019/1185
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2019/1185,
author = {David Butler and Andreas Lochbihler and David Aspinall and Adria Gascon},
title = {Formalising $\Sigma$-Protocols and Commitment Schemes using CryptHOL},
howpublished = {Cryptology {ePrint} Archive, Paper 2019/1185},
year = {2019},
url = {https://eprint.iacr.org/2019/1185}
}