José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe · 6 authors
Developers building cryptography into security-sensitive applications face a daunting task. Not only must they understand the security guarantees delivered by the constructions they choose, they must also implement and combine them correctly and efficiently. Cryptographic compilers free developers from this task by turning high-level specifications of security goals into efficient implementations. Yet, trusting such tools is hard as they rely on complex mathematical machinery and claim security properties that are subtle and difficult to verify. In this paper we present ZKCrypt, an optimizing cryptographic compiler achieving an unprecedented level of assurance without sacrificing practicality for a comprehensive class of cryptographic protocols, known as Zero-Knowledge Proofs of Knowledge. The pipeline of ZKCrypt integrates purpose-built verified compilers and verifying compilers producing formal proofs in the CertiCrypt framework. By combining the guarantees delivered by each stage, ZKCrypt provides assurance that the output implementation securely realizes the abstract proof goal given as input. We report on the main characteristics of ZKCrypt, highlight new definitions and concepts at its foundations, and illustrate its applicability through a representative example of an anonymous credential system
One of the most fundamental goals in cryptography is to design protocols that remain secure when adversarial participants can engage in arbitrary malicious behavior. In 1986, Goldreich, Micali, and Wigderson presented a powerful paradigm for designing such protocols: their approach reduced the task of designing secure protocols to designing protocols that only guarantee security against “honest-but-curious” participants. By making use of zero-knowledge proofs, the GMW paradigm enforces honest behavior without compromising secrecy. Over the past two decades, this approach has been the dominant paradigm for cryptographic protocol design, based on zero-knowledge protocols based on computational hardness assumptions. In this work, we describe a new general paradigm/protocol compiler for secure protocol design known as the IPS compiler, that departs considerably from the GMW framework, and provides a method for obtaining efficient protocols with information-theoretic security guarantees in settings where appropriate channels exist. This new approach also reduces the task of designing secure protocols to designing protocols that only guarantee security against honest-but-curious participants. However, the new approach avoids the use of zero-knowledge proofs, and instead makes use of multi-party protocols in a much simpler setting - where the majority of participants are completely honest (such multi-party protocols can exist with information-theoretic security guarantees without assuming any special channels). The IPS paradigm yields protocols that rely on Oblivious Transfer channels (OT) as a building block. This offers a number of advantages in generality and efficiency. In contrast to the GMW paradigm, by avoiding the use of zero-knowledge proofs, the IPS paradigm is able to treat all of its building blocks as “black boxes”. This allows improvement over previous results in the area of secure computation. In particular, the IPS compiler yields conceptually simpler and more efficient ways for basing unconditionally secure cryptography on OT and other noisy channels; more efficient protocols for generating a large number of OTs using a small number of OTs; and secure and efficient protocols which only make a blackbox use of cryptographic primitives or underlying algebraic structures in settings where no such protocols were known before.
In this paper, through introducing the Williams public-key cryptosystem in detail, the analysis of the characteristics of the system, and the combination with zero knowledge proof, we set up a zero-knowledge proof scheme based on Williams public-key cryptosystem. The scheme will enrich the theory of cryptography, and particularly zero-knowledge proof theory.
CertiCrypt is a framework that enables the machine-checked construction and verification of cryptographic proofs in the Coq proof assistant. CertiCrypt instruments the code-based game-based approach to cryptographic proofs, and builds upon many areas, including probability and complexity theory, algebra, semantics of programming languages, and program optimizations. In this thesis, we illustrate the application of CertiCrypt on two examples: the Hashed ElGamal encryption scheme and zero-knowledge protocols. Like previous case studies in CertiCrypt, these examples demonstrate the feasibility of formalizing complex cryptographic proofs. However, using CertiCrypt requires a high level of expertise in Coq, and is time consuming. In order to ease the adoption of formal proofs by the cryptographic community, we develop a semi-automated tool, called EasyCrypt, for elaborating security proofs of cryptographic systems from proof sketches. Proof sketches are checked automatically using SMT solvers and automated theorem provers, and then compiled into verifiable proofs in the CertiCrypt framework. We illustrate the application of EasyCrypt with two examples: the Hashed ElGamal encryption system, and the Cramer-Shoup encryption system. Finally, we extend the language of CertiCrypt with a formalization of polytime functions.
Abstract : Zero-knowledge proofs (ZKPs) are protocols that enable a prover to convince a verifier of the truth of a statement without leaking any other information. The main properties of ZKP include completeness, soundness and zero-knowledge. These features are correlated with each other, and together with the lighter computational requirements, makes zero-knowledge protocols very attractive in authentication service in airborne networks. Although useful, the non-interactive zero-knowledge proofs based on standard cryptographic assumptions used to be inefficient and not useful in practice. The use of pairing-based ZKP on elliptic curves can potentially enhance the security strength of the system. Besides these advantages, pairing-based ZKPs can also integrate smoothly with other pairing-based cryptographic schemes (e.g., identity-based encryption, pairing-based signatures, key agreement, and proxy re-encryption) making the combined schemes quite efficient.
We introduce the concept of identity-based encryption (IBE) with master key-dependent chosenplaintext (mKDM-sID-CPA) security. These are IBE schemes that remain secure even after the adversary sees encryptions, under some initially selected identities, of functions of the master secret key(s). We then propose a generic construction of chosen-ciphertext secure key-dependent encryption (KDM-CCA) schemes in the public key setting starting from mKDM-sID-CPA secure IBE schemes. This is reminiscent to the celebrated work by Canetti, Halevi and Katz (Eurocrypt 2004) on the traditional key-oblivious setting. Previously only one generic construction of KDM-CCA secure public key schemes was known, due to Camenisch, Chandran and Shoup (Eurocrypt 2009), and it required non-interactive zero knowledge proofs (NIZKs). Our transformation shows that NIZKs are not intrinsic to KDM-CCA public key encryption. Additionally, we are able to instantiate our new concept under the Rank assumption on pairing groups and for affine functions of the secret keys. The scheme builds on previous work by Boneh, Halevi, Hamburg and Ostrovsky (Crypto 2008). Our concrete schemes are only able to provide security against a bounded number of encryption queries, which is enough in some practical scenarios. As a corollary we obtain a KDM-CCA secure public key encryption scheme, in the standard model, whose security reduction to a static assumption is independent of the number of challenge queries. As an independent contribution, we give new and better reductions between the Rank problem (previously named as Matrix DDH problem) and the Decisional Linear and the Decisional 3-Party Diffie-Hellman problems.
Dana Dachman-Soled, Abhishek Jain, Yael Tauman Kalai, Adriana López-Alt
The Fiat-Shamir paradigm [CRYPTO’86] is a heuristic for converting 3-round identification schemes into signature schemes, and more generally, for collapsing rounds in public-coin interactive protocols. This heuristic is very popular both in theory and in practice, and many researchers have studied its security (and insecurity). In this work, we continue this study. As our main result, we show that for many well studied interactive proofs (and arguments) the soundness of the Fiat-Shamir heuristic cannot be proven via a black-box reduction to any falsifiable assumption. Previously, the insecurity of this paradigm was exemplified only when applied to interactive arguments (as opposed to proofs). Using similar techniques, we also show a black-box impossibility result for Micali’s CSproofs [FOCS’94]. Namely, we prove that there exist PCPs such that for “sufficiently hard” NP languages, Micali’s CS-proof cannot be proven sound via black-box reduction to any falsifiable assumption. These results are obtained by extending the impossibility of two-message zero knowledge protocols due to Goldreich and Oren [J. Cryptology’94].
Abstract. In TCC 2007, Adida and Wikström proposed a novel approach to shuffle, called a public shuffle, in which a shuffler can perform shuffle publicly without needing information kept secret. Their scheme uses an encrypted permutation matrix to shuffle ciphertexts publicly. This approach significantly reduces the cost of constructing a mix-net to verifiable joint decryption. Though their method is successful in making shuffle to be a public operation, their scheme still requires that some trusted parties should choose a permutation to be encrypted and construct zero-knowledge proofs on the well-formedness of this permutation. In this paper, we propose a method to construct a public shuffle without relying on permutations and randomizers generated privately: Given an n-tuple of ciphertext (c1,..., cn), our shuffle algorithm computes fi(c1,..., cn) for i = 1,..., ℓ where each fi(x1,..., xn) is a symmetric polynomial in x1,..., xn. Depending on the symmetric polynomials we use, we propose two concrete constructions. One is to use ring homomorphic encryption with constant ciphertext complexity and the other is to use simple ElGamal encryption with linear ciphertext complexity in the number of senders. Both constructions are free of zero-knowledge proofs and publicly verifiable.
When initializing cryptographic systems or running cryptographic protocols, the randomness of critical parameters, like keys or key components, is one of the most crucial aspects. But, randomly chosen parameters come with the intrinsic chance of duplicates, which finally may cause cryptographic systems including RSA, ElGamal and Zero-Knowledge proofs to become insecure. When concerning digital identifiers, we need uniqueness in order to correctly identify a specific action or object. Unfortunately we also need randomness here. Without randomness, actions become linkable to each other or to their initiator’s digital identity. So ideally the employed (cryptographic) parameters should fulfill two potentially conflicting requirements simultaneously: randomness and uniqueness. This article proposes an efficient mechanism to provide both attributes at the same time without highly constraining the first one and never violating the second one. After defining five requirements on random number generators and discussing related work, we will describe the core concept of the generation mechanism. Subsequently we will prove the postulated properties (security, randomness, uniqueness, efficiency and privacy protection) and present some application scenarios including system-wide unique parameters, cryptographic keys and components, identifiers and digital pseudonyms.
In FOCS 2001, Barak, Goldreich, Goldwasser and Lindell conjectured that the existence of ZAPs, introduced by Dwork and Naor in FOCS 2000, could lead to the design of a zeroknowledge proof system that is secure against both resetting provers and resetting verifiers. Their conjecture has been proven true by Deng, Goyal and Sahai in FOCS 2009 where both ZAPs and collision-resistant hash functions (CRHFs, for short) play a fundamental role. In this paper, we present a new technique that allows us to prove that simultaneously resettable zero knowledge can be achieved by relying on CRHFs only. Our construction therefore goes beyond the conjecture of Barak et al. bypassing the (demanding) use of ZAPs, that in turn require double enhanced trapdoor permutations (DTPs, for short). More specifically, we present the following results: 1. We construct the first resettably-sound resettable witness indistinguishable (rsrWI, for short) argument for NP based on CRHFs. Our construction exploits a new technique that we call “soundness upgrade”. In order to upgrade stand-alone soundness to resettable soundness, we use the lower bound proved by Rosen in CRYPTO 2000 on the round complexity of black-box concurrent zero knowledge. Moreover our rsrWI argument is an argument of knowledge (AoK, for short). 2. As an application of the above result, we obtain the main theorem of this work: we prove (constructively) the existence of an argument system that is both resettable zero knowledge and resettably sound under the sole assumption that CRHFs exist. Our results improve the state-of-the-art, and, perhaps even more importantly, provide a novel tool for the design of resettably-secure protocols. We also show a novel way to use protocol lower bounds in constructive protocol design.
Melissa Chase, Markulf Kohlweiss, Anna Lysyanskaya, Sarah Meiklejohn
Depending on the application, malleability in cryptography can be viewed as either a flaw or — especially if sufficiently understood and restricted — a feature. In this vein, Chase, Kohlweiss, Lysyanskaya, and Meiklejohn recently defined malleable zero-knowledge proofs, and showed how to control the set of allowable transformations on proofs. As an application, they construct the first compact verifiable shuffle, in which one such controlled-malleable proof suffices to prove the correctness of an entire multi-step shuffle. Despite these initial steps, a number of natural open problems remain: (1) their construction of controlled-malleable proofs relies on the inherent malleability of Groth-Sahai proofs and is thus not based on generic primitives; (2) the classes of allowable transformations they can support are somewhat restrictive; and (3) their construction of a compactly verifiable shuffle has proof size O(N 2 + L) (where N is the number of votes and L is the number of mix authorities), whereas in theory such a proof could be of size O(N + L). In this paper, we address these open problems by providing a generic construction of controlledmalleable proofs using succinct non-interactive arguments of knowledge, or SNARGs for short. Our construction has the advantage that we can support a very general class of transformations (as we no longer rely on the transformations that Groth-Sahai proofs can support), and that we can use it to obtain a proof of size O(N + L) for the compactly verifiable shuffle.
Sebastian Faust, Markulf Kohlweiss, Giorgia Azzurra Marson, Daniele Venturi
The Fiat-Shamir transform is a well studied paradigm for removing interaction from publiccoin protocols. We investigate whether the resulting non-interactive zero-knowledge (NIZK) proof systems also exhibit non-malleability properties that have up to now only been studied for NIZK proof systems in the common reference string model: first, we formally define simulation soundness and a weak form of simulation extraction in the random oracle model (ROM). Second, we show that in the ROM the Fiat-Shamir transform meets these properties under lenient conditions. A consequence of our result is that, in the ROM, we obtain truly efficient non malleable NIZK proof systems essentially for free. Our definitions are sufficient for instantiating the Naor-Yung paradigm for CCA2-secure encryption, as well as a generic construction for signature schemes from hard relations and simulation-extractable NIZK proof systems. These two constructions are interesting as the former preserves both the leakage resilience and key-dependent message security of the underlying CPA-secure encryption scheme, while the latter lifts the leakage resilience of the hard relation to the leakage resilience of the resulting signature scheme.