Cryptology ePrint Archive: Report 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.

Category / Keywords: foundations / Formal methods, commitment schemes, sigma protocols

Date: received 11 Oct 2019

Contact author: dbutler at turing ac uk

Available format(s): PDF | BibTeX Citation

Version: 20191015:074051 (All versions of this report)

Short URL: ia.cr/2019/1185


[ Cryptology ePrint archive ]