Welcome to the resource topic for 2019/1185
Title:
Formalising \Sigma-Protocols and Commitment Schemes using CryptHOL
Authors: David Butler, Andreas Lochbihler, David Aspinall, Adria Gascon
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.
ePrint: https://eprint.iacr.org/2019/1185
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .