A Machine-Checked Formalization of Sigma-Protocols

Gilles Barthe (1) , Daniel Hedin (1) , Santiago Zanella-Béguelin (1) , Benjamin Grégoire (2) , Sylvain Heraud (2)

1 Institute IMDEA Software [Madrid]
2 MARELLE - Mathematical, Reasoning and Software

Zero-knowledge proofs have a vast applicability in the domain of cryptography, stemming from the fact that they can be used to force potentially malicious parties to abide by the rules of a protocol, without forcing them to reveal their secrets. $\Sigma$-protocols are a class of zero-knowledge proofs that can be implemented efficiently and that suffice for a great variety of practical applications. This paper presents a first machine-checked formalization of a comprehensive theory of Sigma-protocols. The development includes basic definitions, relations between different security properties that appear in the literature, and general composability theorems. We show its usefulness by formalizing---and proving the security---of concrete instances of several well-known protocols. The formalization builds on CertiCrypt, a framework that provides support to reason about cryptographic systems in the Coq proof assistant, and that has been previously used to formalize security proofs of encryption and signature schemes

Domaines: Cryptographie et sécurité [cs.CR]

Gilles Barthe, Daniel Hedin, Santiago Zanella-Béguelin, Benjamin Grégoire, Sylvain Heraud. A Machine-Checked Formalization of Sigma-Protocols. CSF'10, Jul 2010, Edinburgh, Sweden. pp.246-260, ⟨10.1109/CSF.2010.24⟩. ⟨inria-00552886⟩