Contracts enable mutually suspicious parties to cooperate safely through the exchange of rights. Smart contracts are programs whose behavior enforces the terms of the contract. This paper shows how such contracts can be specified elegantly and executed safely, given an appropriate distributed, secure, persistent, and ubiquitous computational fabric. JavaScript provides the ubiquity but must be significantly extended to deal with the other aspects. The first part of this paper is a progress report on our efforts to turn JavaScript into this fabric. To demonstrate the suitability of this design, we describe an escrow exchange contract implemented in 42 lines of JavaScript code.
In this thesis, we construct an implementation of succinct non-interactive zero knowledge argument system. A non-interactive zero knowledge argument system is a protocol for a party (usually known as Prover) to provide a proof of knowledge to the solution of a statement to other parties (usually known as Verifier). The argument system will be able to provide such proof without leaking any other information regarding the solution. The non-interactivity allows such argument system to be done without requiring interaction between the parties involved. The statement that is proven in this work is the circuit satisfiability problem. The circuit satisfiability problem is a problem of deciding whether there exists an input that can make the final output of a circuit to be true. The argument system is based on Lipmaa's work \\cite{eprint2013:Lipmaa:NIZKSPECC} which uses span programs and linear error-correcting codes in its construction. We also try to give a very general explanation on zero knowledge argument system along the way in order to provide a simple concept to people encountering the notion for the first time. The argument system we attempt to construct is the non-adaptive version of the argument system. This version is useful for verifiable computation as pointed out by \\cite{Pinnochio2013:Parno} apart from its zero knowledge behavior. We begin by giving an overview on non-interactive zero knowledge, followed by span programs. We then proceed to describe on how to represent the circuit satisfiability problem using the mentioned tool. We present our implementation afterwards, listing out the libraries and implementation details that matters. We conclude by providing a speed measurement and possible future improvements of this work.
Abstract. Consider a joint distribution (X,A) on a set X Ă{0, 1}â. We show that for any family F of distinguishers f: X Ă {0, 1}â â {0, 1}, there exists a simulator h: X â {0, 1}â such that 1. no function in F can distinguish (X,A) from (X,h(X)) with advantage Ç«, 2. h is only O(23âÇ«â2) times less efficient than the functions in F. For the most interesting settings of the parameters (in particular, the cryptographic case where X has superlogarithmic min-entropy, Ç«> 0 is negligible and F consists of circuits of polynomial size), we can make the simulator h deterministic. As an illustrative application of this theorem, we give a new security proof for the leakage-resilient stream-cipher from Eurocryptâ09. Our proof is simpler and quantitatively much better than the original proof using the dense model theorem, giving meaningful security guarantees if instantiated with a standard blockcipher like AES. Subsequent to this work, Chung, Lui and Pass gave an interactive variant of our main theorem, and used it to investigate weak notions of Zero-Knowledge. Vadhan and Zheng give a more constructive version of our theorem using their new uniform min-max theorem. 1
We consider a class of two-party function evaluation protocols in which the parties are allowed to<br/>use ideal functionalities as well as a set of powerful primitives, namely commitments, homomorphic<br/>encryption, and certain zero-knowledge proofs. We illustrate that with these it is possible to capture<br/>protocols for oblivious transfer, coin- ipping, and generation of multiplication-triple.<br/>We show how any protocol in our class can be compiled to a symbolic representation expressed<br/>as a process in an abstract process calculus, and prove a general computational soundness theorem<br/>implying that if the protocol realises a given ideal functionality in the symbolic setting, then the<br/>original version also realises the ideal functionality in the standard computational UC setting. In<br/>other words, the theorem allows us to transfer a proof in the abstract symbolic setting to a proof in<br/>the standard UC model.<br/>Finally, we show that the symbolic interpretation is simple enough in a number of cases for the<br/>symbolic proof to be partly automated using ProVerif
Eli BenâSasson, Alessandro Chiesa, Eran Tromer, Madars Virza
We design and build a system that enables clients to verify the outputs of programs executed by untrusted servers. A server provides a succinct non-interactive zero-knowledge proof (also known as a zk-SNARK), which the client verifies to ascertain correct execution. The system has two components: a cryptographic proof system for verifying satisfiability of arithmetic circuits, and a circuit generator to translate program executions to such circuits. Our design of both components improves in functionality and efficiency over previous work, as follows. Our circuit generator is the first to be universal: it does not need to know the program, but only a bound on its running time. It is also the first to support programs expressed as code for a von Neumann RISC random-access memory architecture, where programs may use just-in-time compilation and selfmodifying code. Moreover, the dependence on program size is additive (instead of multiplicative as in prior works), allowing efficient verification of large programs. The cryptographic proof system significantly improves proving and verification times, using a new pairing-based cryptographic library tailored to the protocol. We evaluated our system for programs with up to 10,000 instructions, running for up to 32,000 machine steps, each of which can arbitrarily access random-access memory; and demonstrated it executing programs that use just-in-time compilation. Our proofs are 230 bytes long at 80 bits of security, or 288 bytes long at 128 bits of security. Typical verification time is 5 ms, regardless of the original programâs running time.
By analyzing the definition of the platform configuration registers(PCRs) in the trusted computing platform(TCP) by the trusted computing group(TCG) and combining related researches for techniques of data sealing,a method for property representation of the trusted platform.This method not only can fully illustrate all the characteristics of a trusted computing platform is proposed,but also can make the verification process of the properties with the zero-knowledge proof more conveniently.As well known,one major and inherent defect of trusted computing platform is its exposure for user's privacy.Aiming at overcoming such a drawback,a method of data sealing based on property with zero-knowledge proof is proposed.And in this method,a Trusted Third Party is invited to make proof for verifying the trusted platform.The analysis for security of the method is presented and verification is made for it by experiment.Results from the experiment shows that,this method maintains as the same advantages as other existed schemes,whereas only with a small quantity of data cost.Such small data incrementation not only supports unsealing at remote server,but also works well for preventing privacy disclosure in a trusted platform.
Bryan Parno, Jon Howell, Craig Gentry, Mariana Raykova
To instill greater confidence in computations outsourced to the cloud, clients should be able to verify the correctness of the results returned. To this end, we introduce Pinocchio, a built system for efficiently verifying general computations while relying only on cryptographic assumptions. With Pinocchio, the client creates a public evaluation key to describe her computation; this setup is proportional to evaluating the computation once. The worker then evaluates the computation on a particular input and uses the evaluation key to produce a proof of correctness. The proof is only 288 bytes, regardless of the computation performed or the size of the inputs and outputs. Anyone can use a public verification key to check the proof. Crucially, our evaluation on seven applications demonstrates that Pinocchio is efficient in practice too. Pinocchioâs verification time is typically 10ms: 5-7 orders of magnitude less than previous work; indeed Pinocchio is the first general-purpose system to demonstrate verification cheaper than native execution (for some apps). Pinocchio also reduces the workerâs proof effort by an additional 19-60Ă. As an additional feature, Pinocchio generalizes to zero-knowledge proofs at a negligible cost over the base protocol. Finally, to aid development, Pinocchio provides an end-to-end toolchain that compiles a subset of C into programs that implement the verifiable computation protocol. 1
Kai-Min Chung, Edward Lui, Mohammad Mahmoody, Rafael Pass
Goldreich and Oren (JoCâ94) show that only trivial languages have 2-message zero-knowledge arguments. In this note we consider weaker, super-polynomial-time simulation (SPS), notions of zero-knowledge. We present barriers to using black-box reductions for demonstrating soundness of 2-message protocols with efficient prover strategies satisfying SPS zero-knowledge. More precisely, we show that assuming the existence of poly(T (n))-hard one-way functions, the following holds: âą For sub-exponential (or smaller) T (·), polynomial-time black-box reductions cannot be used to prove soundness of 2-message T (·)-simulatable arguments based on any polynomialtime intractability assumption. This matches known 2-message quasi-polynomial-time simulatable arguments using a quasi-polynomial-time reduction (Passâ03), and 2-message exponential-time simulatable proofs using a polynomial-time reduction (Dwork-Naorâ00, Passâ03). âą poly(T (·))-time black-box reductions cannot be used to prove soundness of 2-message strong T (·)-simulatable (efficient prover) arguments based on any poly(T (·))-time intractability assumption; strong T (·)-simulatability means that the output of the simulator is indistinguishable also for poly(T (·))-size circuits. This matches known 3-message strong quasi-polynomial-time simulatable proofs (Blumâ86, Canetti et al â 00).
Xiao Qiang Guo, Li Hong Li, Cui Ling Luo, Yi Shuo Shi
The Bit Commitment (BC) is an important basic agreement in cryptography . The concept was first proposed by the winner of the Turing Award in 1995 ManuelBlum. Bit commitment scheme can be used to build up zero knowledge proof, verified secret sharing, throwing coins etc agreement.Simultaneously and Oblivious Transfer together constitute the basis of secure multi-party computations. Both of them are hotspots in the field of information security. We investigated unconditional secure Quantum Bit Commitment (QBC) existence. And we constructed a new bit commitment model â double prover bit commitment. The Quantum Bit Commitment Protocol can be resistant to errors caused by noise.
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
We present a constant-round concurrent zero-knowledge protocol for NP. Our protocol is sound against uniform polynomial-time attackers, and relies on the existence of families of collision-resistant hash functions, and a new (but in our eyes, natural) falsifiable intractability assumption: Roughly speaking, that Micaliâs non-interactive CS-proofs are sound for languages in P.
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.
Controlled access to confidential information and resources is a critical element in security systems. Role-based access control (RBAC) has gained widespread usage in modern enterprise systems. Extensions have been proposed to RBAC for incorporating spatial constraints into such systems. Several solutions have been proposed for such models and many researchers are now focusing on enforcing system policies. In this paper we propose a security framework for RBAC systems with spatial constraints based on identity-based encryption. In our framework, we use identity-based encryption with zero knowledge proof (ZKP) to provide authentication and information security. We also show how Near Field Communication (NFC) can be used to establish the integrity of a user's proof of location. Simulation results in Java validate our model. Furthermore, security analysis has been done to show how our framework protects against well-known attacks.
Chida and Yamamoto propose a batch proof algorithm to enhance the performance of multiple instances of zero knowledge proof of partial knowledge. When multiple instances of zero knowledge proof of partial knowledge need to be proved simultaneously, their proof algorithm employs a batching mechanism to reduce the cost in computation and communication. Unfortunately, their batch proof algorithm is not sound and vulnerable to an attack, which completely breaks soundness of the proof. More precisely, an adversary can design the multiple partial knowledge statements in a special way such that no matter how he is challenged he can always pass the verification as a prover in the batch proof scheme while he does not have the knowledge he claims. The attack is presented and is formally illustrated to always succeed.
This paper focuses on the robustness of concurrent non-malleable zero-knowledge.Existing concurrent non-malleable zero-knowledge protocols either apply non-black-box techniques,or employ black-box but incorporate a zero-knowledge sub-protocol.Hence when concurrently composed with other protocols,security of these protocols is not preserved or hard to argue.Following the well-known Feige-Shamir style,this paper presents a new construction for concurrent non-malleable zero-knowledge argument system,which is easily composed.This protocol takes the robust non-malleable commitment scheme introduced by Lin and Pass in STOC 2009 and specially designed witness indistinguishable proofs as basic components to achieve non-malleability and robustness.Moreover,this paper applies the oblivious simulation strategy to simulate the view of the adversary,and the proof technique introduced by Lin et al.in Crypto 2010 to analyze the indistinguishability of simulation.Since witness indistinguishability is closed under concurrent composition,the commitment sub-protocol is robust and the is oblivious,when concurrently composed with other protocols,this protocol is easier to work with and analyze.Based on the one-way function assumption,the round complexity of this protocol is super-logarithmic.
In this thesis we present two new type systems for verifying the security of cryptographic protocol models expressed in a spi-calculus and, respectively, of protocol implementations expressed in a concurrent lambda calculus. In this thesis we present two new type systems for verifying the security of cryptographic protocol models expressed in a spi-calculus and, respectively, of protocol implementations expressed in a concurrent lambda calculus. The two type systems combine prior work on refinement types with union and intersection types and with the novel ability to reason statically about the disjointness of types. The increased expressivity enables the analysis of important protocol classes that were previously out of scope for the type-based analyses of cryptographic protocols. In particular, our type systems can statically analyze protocols that are based on zero-knowledge proofs, even in scenarios when certain protocol participants are compromised. The analysis is scalable and provides security proofs for an unbounded number of protocol executions. The two type systems come with mechanized proofs of correctness and efficient implementations.
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 having to implement cryptography on their own by turning high-level specifications of security goals into efficient implementations. Yet, trusting such tools is risky 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 that achieves 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 tightly integrates purpose-built verified compilers and verifying compilers producing formal proofs in the CertiCrypt framework. By combining the guarantees delivered by each stage in the pipeline, ZKCrypt provides assurance that the implementation it outputs securely realizes the high-level 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.
Yi Deng, Juan A. Garay, San Ling, Huaxiong Wang · 5 authors
We consider the problem of whether there exist non-trivial constant-round public-coin zero-knowledge ZK proofs. To date, in spite of high interest in the problem, there is no definite answer to the question. We focus on the type of ZK proofs that admit a universal simulator which handles all malicious verifiers, and show a connection between the existence of such proof systems and a seemingly unrelated program functionality distinguishing problem: for a natural class of constant-round public-coin ZK proofs which we call canonical, since all known ZK protocols fall into this category, a session prefix output by the universal simulator can actually be used to distinguish a non-trivial property of the next-step functionality of the verifier's code.
Our result can be viewed as new evidence against the existence of constant-round public-coin ZK proofs, since the existence of such a proof system will bring about either one of the following: 1 a positive result for the above functionality-distinguishing problem, a typical goal in reverse-engineering attempts, commonly believed to be notoriously hard, or 2 a major paradigm shift in simulation strategies, beyond the only known straight-line simulation technique applicable to their argument counterpart, as we also argue. Note that the earlier negative evidence on constant-round public-coin ZK proofs is Barack, Lindell and Vadhan [FOCS 2003]'s result, which was based on the incomparable assumption of the existence of certain entropy-preserving hash functions, now known not to be achievable from standard assumptions via black-box reduction.
The core of our technical contribution is showing that there exists a single verifier step for constant-round public-coin ZK proofs whose functionality rather than its code is crucial for a successful simulation. This is proved by combining a careful analysis of the behavior of a set of verifiers in the above protocols and during simulation, with an improved structure-preserving version of the well-known Babai-Moran Speedup de-randomization Theorem, a key tool of independent interest.
If all applications could be loaded at the start this would boil down to information flow analysis for which many solutions exist, but this is precisely what we want to overcome. When applications are not known in advance and can be updated asynchronously and possibly without connection to trusted third parties, we must preserve the security policies of the various owners of the applets during such autonomous evolution. This chapter illustrates the extension of the Security-by-Contract approach from mobile phones to smart cards: Security-by-Contract is based on the loading time application certification on the card that will enable the card to make autonomous decisions on application and policy updates while ensuring the compliance of every change of the platform with the security policy of each applicationâs owner.