We study the problem of building non-interactive proof systems modularly by linking small specialized SNARKs in a lightweight manner. Our motivation is both theoretical and practical. On the theoretical side, modular SNARK designs would be flexible and reusable. Also, previous works (e.g., Geppetto) consider They have been successfully employed in previous works.(cite prev papers ). These approaches, however, tend to be ad-hoc and to reinventing the wheel. We propose to fill this gap. In practice, specialized SNARKs have the potential to be more efficient than general-purpose schemes, on which most existing works have focused. If a computation naturally presents different components (e.g. one arithmetic circuit and one boolean circuit), a general-purpose scheme would homogenize them to a single representation with a subsequent cost in performance. Through a modular approach one could instead exploit the nuances of a computation and choose the best gadget for each component. Our contribution is LegoSNARK, a toolbox (or framework) for commit-and-prove zkSNARKs (CP-SNARKs) that includes: 1) General composition tools: build new CP-SNARKs from proof gadgets for basic relationssimply. Formalize notion of cc-SNARK. 2) A lifting tool: a compiler to add commit-and-prove capabilities to a broad class of existing zkSNARKsefficiently. This makes them interoperable (linkable) within the same computation. For example, one QAP-based scheme can be used prove one component; another GKR-based scheme can be used to prove another. 3) A collection of succinct proof gadgets for a variety of relations. Additionally, through our framework and gadgets, we are able to obtain new succinct proof systems. Notably: -- LegoGro16, a commit-and-prove version of Groth16 zkSNARK, that operates over data committed with a classical Pedersen vector commitment, and that achieves a 5000Ă speedup in proving time. -- LegoUAC, a pairing-based SNARK for arithmetic circuits that has a universal, circuit-independent, CRS, and proving time linear in the number of circuit gates (vs. the recent scheme of Groth et al. (CRYPTO'18) with quadratic CRS and quasilinear proving time). -- LegoMM, a CP-SNARK for matrix multiplication that achieves optimal proving complexity.
Blockchain systems and smart contracts provide ways to securely implement multi-party transactions without the use of trusted intermediaries, which currently underpin many commercial transactions. However, they do so by transferring trust to computer systems, raising the question of whether code can be trusted. Experience with high value losses resulting from incorrect code has already shown that formal verification of smart contracts is likely to be beneficial. This note investigates the specification and verification of a simple form of multi-party transaction, atomic swaps. It is argued that logics with the ability to express properties of strategies of players in a multi-agent setting are conceptually useful for this purpose, although ultimately, for our specific examples, the less expressive setting of temporal logic suffices for verification of concrete implementations. This is illustrated through a number of examples of the use of a model checker to verify atomic swap smart contracts in on-chain and cross-chain settings.
Reasoning about commutativity between data-structure operations is an important problem with applications including parallelizing compilers, optimistic parallelization and, more recently, Ethereum smart contracts. There have been research results on automatic generation of commutativity conditions, yet we are unaware of any fully automated technique to generate conditions that are both sound and effective. We have designed such a technique, driven by an algorithm that iteratively refines a conservative approximation of the commutativity (and non-commutativity) condition for a pair of methods into an increasingly precise version. The algorithm terminates if/when the entire state space has been considered, and can be aborted at any time to obtain a partial yet sound commutativity condition. We have generalized our work to left-/right-movers and proved relative completeness. We describe aspects of our technique that lead to useful commutativity conditions, including how predicates are selected during refinement and heuristics that impact the output shape of the condition. We have implemented our technique in a prototype open-source tool Servois. Our algorithm produces quantifier-free queries that are dispatched to a back-end SMT solver. We evaluate Servois through two case studies: (i) We synthesize commutativity conditions for a range of data structures including Set, HashTable, Accumulator, Counter, and Stack. (ii) We consider an Ethereum smart contract called BlockKing, and show that Servois can detect serious concurrency-related vulnerabilities and guide developers to construct robust and efficient implementations.
In multi-prover interactive proofs (MIPs), the verifier can provide non-local resources for the provers intrinsically. In most cases, this is undesirable. Existing proofs of soundness do not account for the verifier's non-local potential. We show that this may be a problem for many MIPs. We provide a solution by constructing a generalization of the MIP model, of which standard MIPs are a special case. This new model accounts for both the prover and the verifier's non-local correlations. A new property of multi-prover zero-knowledge naturally emerges as a result.
This paper outlines key design principles of Scilla---an intermediate-level language for verified smart contracts. Scilla provides a clean separation between the communication aspect of smart contracts on a blockchain, allowing for the rich interaction patterns, and a programming component, which enjoys principled semantics and is amenable to formal verification. Scilla is not meant to be a high-level programming language, and we are going to use it as a translation target for high-level languages, such as Solidity, for performing program analysis and verification, before further compilation to an executable bytecode. We describe the automata-based model of Scilla, present its programming component and show how contract definitions in terms of automata streamline the process of mechanised verification of their safety and temporal properties.
The existing multi-prover interactive proof framework suffers from incompleteness in terms of soundness and zero-knowledge that is not completely addressed in the literature. The problem is that the existing definitions of what is local, entangled and no-signalling are not rich enough to capture the full generality of multi-prover interaction. In general, existing proofs do not take into account possible changes in locality either during a protocol's execution or when protocols are composed together. This is especially problematic for zero-knowledge, as composing commitments is the only known way of achieving zero-knowledge outside of some NP-intermediate languages.
In this work, we introduce the locality hierarchy for multiparty (multi-round) interaction, and for the first time a complete definition of multi-round multiparty no-signalling distributions and strategies. Within this framework, we define the locality of a protocol which involves the provers, verifiers, simulators and distinguishers. We show that an existing protocol for NEXP [BFL90] and a zero-knowledge variant we introduce are sound in a local sense, but are zero-knowledge in a sense that is even stronger than usually understood. All prior claims of zero-knowledge proofs in the multi-prover model were actually incorrect. Finally, we present similar constructions for entangled and no-signalling prover sets for NEXP and EXP based on [IV12] and [KRR14] using new multi-prover commitment schemes.
Simplicity is a typed, combinator-based, functional language without loops and recursion, designed to be used for crypto-currencies and blockchain applications. It aims to improve upon existing crypto-currency languages, such as Bitcoin Script and Ethereum's EVM, while avoiding some of the problems they face. Simplicity comes with formal denotational semantics defined in Coq, a popular, general purpose software proof assistant. Simplicity also includes operational semantics that are defined with an abstract machine that we call the Bit Machine. The Bit Machine is used as a tool for measuring the computational space and time resources needed to evaluate Simplicity programs. Owing to its Turing incompleteness, Simplicity is amenable to static analysis that can be used to derive upper bounds on the computational resources needed, prior to execution. While Turing incomplete, Simplicity can express any finitary function, which we believe is enough to build useful ``smart contracts'' for blockchain applications.
Several Multi-Prover Interactive Proofs (MIPs) found in the literature contain proofs of soundness that are lacking. This was first observed [1] in which a notion of Prover isolation is defined to partly address the issue. Furthermore, some existing Zero-Knowledge MIPs suffer from a catastrophic flaw: they outright allow the Provers to communicate via the Verifier. Consequently, their soundness claims are now seriously in doubt, if not plain wrong. This paper outlines the lack of isolation and numerous other issues found in the (ZK)MIP literature. A follow-up paper will resolve most of these issues in detail.
Quantum information and computation provide a fascinating twist on the notion of proofs in computational complexity theory. For instance, one may consider a quantum computational analogue of the complexity class NP, known as QMA, in which a quantum state plays the role of a proof (also called a certificate or witness), and is checked by a polynomial-time quantum computation. For some problems, the fact that a quantum proof state could be a superposition over exponentially many classical states appears to offer computational advantages over classical proof strings. In the interactive proof system setting, one may consider a verifier and one or more provers that exchange and process quantum information rather than classical information during an interaction for a given input string, giving rise to quantum complexity classes such as QIP, QSZK, and QMIP* that represent natural quantum analogues of IP, SZK, and MIP. While quantum interactive proof systems inherit some properties from their classical counterparts, they also possess distinct and uniquely quantum features that lead to an interesting landscape of complexity classes based on variants of this model. In this survey we provide an overview of many of the known results concerning quantum proofs, computational models based on this concept, and properties of the complexity classes they define. In particular, we discuss non-interactive proofs and the complexity class QMA, single-prover quantum interactive proof systems and the complexity class QIP, statistical zero-knowledge quantum interactive proof systems and the complexity class QSZK, and multiprover interactive proof systems and the complexity classes QMIP, QMIP*, and MIP*.
Akari, Takuzu, Kakuro and KenKen are logic games similar to Sudoku. In Akari, a labyrinth on a grid has to be lit by placing lanterns, respecting various constraints. In Takuzu a grid has to be filled with 0's and 1's, while respecting certain constraints. In Kakuro a grid has to be filled with numbers such that the sums per row and column match given values; similarly in KenKen a grid has to be filled with numbers such that in given areas the product, sum, difference or quotient equals a given value. We give physical algorithms to realize zero-knowledge proofs for these games which allow a player to show that he knows a solution without revealing it. These interactive proofs can be realized with simple office material as they only rely on cards and envelopes. Moreover, we formalize our algorithms and prove their security.
The power of linear and affine logic lies in their ability to model state change. However, in a trustless, peer-to-peer setting, it is difficult to force principals to commit to state changes. We show how to solve the peer-to-peer affine commitment problem using a generalization of Bitcoin in which transactions deal in types rather than numbers. This has applications to proof-carrying authorization and mechanically executable contracts. Importantly, our system can be---and is---implemented on top of the existing Bitcoin network, so there is no need to recruit computing power to a new protocol.
The standard of proof in criminal trials in many liberal democracies is proof beyond a reasonable doubt, the BARD standard. It is customary to describe it, when putting a number on it, as requiring that the fact finder be at least 90% certain, after considering the evidence, that the defendant is guilty. Strikingly, no good reason has yet been offered in defense of using that standard. A number of non-consequentialist justifications that aim to support an even higher standard have been offered; all are morally unsound. Meanwhile, consequentialist arguments plausibly support a substantially lower standard â in some cases so low as to undermine the idea that punishment is what is at stake. In this paper, I offer a new retributive justification that supports excluding the instrumental benefits of punishment from the balance that sets the standard. The resulting balance supports a standard arguably in the ballpark of the customary understanding of BARD: a standard requiring that the fact finder have a high, though not maximally high, degree of confidence that the defendant is guilty.
A probabilistically Checkable Proof (PCP) allows a randomized verifier, with oracle access to a purported proof, to probabilistically verify an input statement of the form âx â Lâ by querying only few bits of the proof. A PCP of proximity (PCPP) has the additional feature of allowing the verifier to query only few bits of the input x, where if the input is accepted then the verifier is guaranteed that (with high probability) the input is close to some xâČ â L.
Single-prover interactive proofs can recognize PSPACE; if certain complexity assumptions are made, they can do so in zero-knowledge. Generalizing to multiple non-communicating provers extends this class to NEXP, and at the same time removes the complexity assumption needed for zero-knowledge. \n \nHowever, it was recently discovered that the non-communication condition might be insufficient to guarantee soundness. The provers can form joint randomness through non-local computation without communicating. This could break protocols that rely on the statistical independence of the provers. \n \nIn this work, we analyze multi-prover interactive proofs under the constraint of statistical isolation which prohibits non-local computation. We show that there exists perfect zero-knowledge proofs for NEXP under statistical isolation.
We develop a non-interactive proof-system which we call âMetaproof â (”-NIZK proof system); it provides a proof of âthe existence of a proof to a statementâ. This metamathematical notion indeed seems redundant when we deal with proving N P statements, but in the context of zero-knowledge theory and cryptography it has a large variety of applications. Combined with another tool we develop which we call âon-line simulatable NIZK proofsystemâ, it is the key tool used to solve the open problem of the existence of a many prover non-interactive zero-knowledge system (MP-NIZK proof system). This problem was presented by Micali when the important notion of non-interactive zero-knowledge proofs (NIZK) was first suggested and implemented for a sole prover. The solution immensely enlarges the domain of applications of the NIZK model. The work also provides a new connection between bounded (single-theorem) non-interactive zero-knowledge proofs and the unbounded (multi-theorem) one. This may help in reducing the complexity assumption upon which to base NIZK systems. Remark: This is a full version (with more details, more material, and with proofs) of the Crypto 1990 paper on Metaproof. Over the years, the concept has been used and reinvented for specific settings beyond the original ones, by others; (which has made it more useful). Recently, we were asked about this paper and about details, so here they are! For historical reasons, except for this remark, this version is presented as it was in the above mentioned date under the above affiliations, though we did not pursue publication before! 1 1