You are looking at a specific version 20120223:214118 of this paper. See the latest version.

Paper 2012/081

Computational Soundness of Symbolic Zero-knowledge Proofs: Weaker Assumptions and Mechanized Verification

Michael Backes and Fabian Bendun and Dominique Unruh

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 crypto- graphic 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 com- putational 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.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Unknown where it was published
Keywords
symbolic zero-knowledgecomputational soundnessweaker assumptionsmechanized proofs
Contact author(s)
bendun @ cs uni-saarland de
History
2012-02-23: received
Short URL
https://ia.cr/2012/081
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.