(2013) Computational Soundness of Symbolic Zero-Knowledge Proofs: Weaker Assumptions and Mechanized Verification.
Abstract
The abstraction of cryptographic operations by term algebras, called symbolic models, is essential in almost all tool-supported methods for analyzing security protocols. Significant progress was made in proving that symbolic models offering basic cryptographic operations such as encryption and digital signatures can be sound with respect to actual cryptographic realizations and security definitions. Even abstractions of sophisticated modern cryptographic primitives such as zero-knowledge (ZK) proofs were shown to have a computationally sound cryptographic realization, but only in ad-hoc formalisms and at the cost of placing strong assumptions on the underlying cryptography, which leaves only highly inefficient realizations. In this paper, we make two contributions to this problem space. First, we identify weaker cryptographic assumptions that we show to be sufficient for computational soundness of symbolic ZK proofs. These weaker assumptions are fulfilled by existing efficient ZK schemes as well as generic ZK constructions. Second, we conduct all computational soundness proofs in CoSP, a recent framework that allows for casting computational soundness proofs in a modular manner, independent of the underlying symbolic calculi. Moreover, all computational soundness proofs conducted in CoSP automatically come with mechanized proof support through an embedding of the applied-pi calculus.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Additional Information: | pub_id: 169 Bibtex: BaBeUn13 URL date: None |
| Uncontrolled Keywords: | computational soundness,zero-knowledge protocols |
| Divisions: | Michael Backes (InfSec) |
| Depositing User: | Sebastian Weisgerber |
| Date Deposited: | 26 Jul 2017 10:29 |
| Last Modified: | 18 Jul 2019 12:09 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/256 |
Actions
Actions (login required)
 |
View Item |