You are looking at a specific version 20191015:074051 of this paper. See the latest version.

Paper 2019/1185

Formalising $\Sigma$-Protocols and Commitment Schemes using CryptHOL

David Butler and Andreas Lochbihler and David Aspinall and 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.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Preprint. MINOR revision.
Keywords
Formal methodscommitment schemessigma protocols
Contact author(s)
dbutler @ turing ac uk
History
2019-10-15: received
Short URL
https://ia.cr/2019/1185
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.