A Machine-Checked Formalization of Sigma-Protocols
- 1 July 2010
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 5978 (10636900) , 246-260
- https://doi.org/10.1109/csf.2010.24
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. Σ-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 Σ-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.Keywords
This publication has 20 references indexed in Scilit:
- Achieving Security Despite Compromise Using Zero-knowledgePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2009
- Certificate translation for optimizing compilersACM Transactions on Programming Languages and Systems, 2009
- Proofs of randomized algorithms in CoqScience of Computer Programming, 2009
- Type-checking zero-knowledgePublished by Association for Computing Machinery (ACM) ,2008
- Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation ProtocolPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2008
- Formal certification of a compiler back-end orPublished by Association for Computing Machinery (ACM) ,2006
- Computationally Sound, Automated Proofs for Security ProtocolsPublished by Springer Nature ,2005
- Strengthening Zero-Knowledge Protocols Using SignaturesPublished by Springer Nature ,2003
- Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)*Journal of Cryptology, 2002
- On the Existence of Bit Commitment Schemes and Zero-Knowledge ProofsPublished by Springer Nature ,2001