A Machine-Checked Formalization of Sigma-Protocols - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

## A Machine-Checked Formalization of Sigma-Protocols

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

#### Abstract

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

### Dates and versions

inria-00552886 , version 1 (10-01-2011)

### Identifiers

• HAL Id : inria-00552886 , version 1
• DOI :

### Cite

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⟩

### Export

BibTeX TEI Dublin Core DC Terms EndNote Datacite

259 View