Follow blockchain research across journals, conferences, and preprint repositories.
120 results · page 4 of 5
James Chapman, Roman Kireev, Chad Nester, Philip Wadler
No abstract is available for this record.
Matthew Coudron, William Slofstra
We study the problem of approximating the commuting-operator value of a two-player non-local game. It is well-known that it is $\mathrm{NP}$-complete to decide whether the classical value of a non-local game is 1 or $1- ε$. Furthermore, as long as $ε$ is small enough, this result does not depend on the gap $ε$. In contrast, a recent result of Fitzsimons, Ji, Vidick, and Yuen shows that the complexity of computing the quantum value grows without bound as the gap $ε$ decreases. In this paper, we show that this also holds for the commuting-operator value of a game. Specifically, in the language of multi-prover interactive proofs, we show that the power of $\mathrm{MIP}^{co}(2,1,1,s)$ (proofs with two provers, one round, completeness probability $1$, soundness probability $s$, and commuting-operator strategies) can increase without bound as the gap $1-s$ gets arbitrarily small. Our results also extend naturally in two ways, to perfect zero-knowledge protocols, and to lower bounds on the complexity of computing the approximately-commuting value of a game. Thus we get lower bounds on the complexity class $\mathrm{PZK}$-$\mathrm{MIP}^{co}_δ(2,1,1,s)$ of perfect zero-knowledge multi-prover proofs with approximately-commuting operator strategies, as the gap $1-s$ gets arbitrarily small. While we do not know any computable time upper bound on the class $\mathrm{MIP}^{co}$, a result of the first author and Vidick shows that for $s = 1-1/\text{poly}(f(n))$ and $δ= 1/\text{poly}(f(n))$, the class $\mathrm{MIP}^{co}_δ(2,1,1,s)$, with constant communication from the provers, is contained in $\mathrm{TIME}(\exp(\text{poly}(f(n))))$. We give a lower bound of $\mathrm{coNTIME}(f(n))$ (ignoring constants inside the function) for this class, which is tight up to polynomial factors assuming the exponential time hypothesis.
Jean‐Guillaume Dumas, Pascal Lafourcade, Daiki Miyahara, Takaaki Mizuki · 6 authors
No abstract is available for this record.
Anshu Shukla, Swarup Kumar Mohalik, Ramamurthy Badrinath
Intelligent Cyber-physical systems can be modelled as multi-agent systems\nwith planning capability to impart adaptivity for changing contexts. In such\nmulti-agent systems, the protocol for plan execution must result in the proper\ncompletion and ordering of actions in spite of their distributed execution.\nHowever, in untrusted scenarios, there is a possibility of agents not\nrespecting the protocol either due to faults or due to malicious reasons\nthereby resulting in plan failure. In order to prevent such situations, we\npropose to implement the execution of agents through smart contracts. This\npoints to a generic architecture seamlessly integrating intelligent\nplanning-based CPS and smart-contracts.\n
Anshu Shukla, Swarup Kumar Mohalik, Ramamurthy Badrinath
Intelligent Cyber-physical systems can be modelled as multi-agent systems with planning capability to impart adaptivity for changing contexts. In such multi-agent systems, the protocol for plan execution must result in the proper completion and ordering of actions in spite of their distributed execution. However, in untrusted scenarios, there is a possibility of agents not respecting the protocol either due to faults or due to malicious reasons thereby resulting in plan failure. In order to prevent such situations, we propose to implement the execution of agents through smart contracts. This points to a generic architecture seamlessly integrating intelligent planning-based CPS and smart-contracts.
Ron van der Meyden
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.
Zaynah Dargaye, Antonella Del Pozzo, Sara Tucci-Piergiovanni
The paper presents Pluralize a formal logical framework able to extend the execution of blockchain transactions to events coming from external oracles, like external time, sensor data, human-made declarations, etc. These events are by essence non-reliable, since transaction execution can be triggered by information whose veracity cannot be established by the blockchain. To overcome this problem, the language features a first-order logic and an authority algebra to allow formal reasoning and establish accountability of agents for blockchain-enabled transactions. We provide an accountability model that allows to formally prove the accountability of agents by a formal proof locally executable by each agent of the blockchain.
Anton Setzer
We present two models of the block chain of Bitcoin in the interactive theorem prover Agda. The first one is based on a simple model of bank accounts, while having transactions with multiple inputs and outputs. The second model models transactions, which refer directly to unspent transaction outputs, rather than user accounts. The resulting blockchain gives rise to a transaction tree. That model is formalised using an extended form of induction-recursion, one of the unique features of Agda. The set of transaction trees and transactions is defined inductively, while simultaneously recursively defining the list of unspent transaction outputs. Both structures model standard transactions, coinbase transactions, transaction fees, the exact message to be signed by those spending money in a transaction, block rewards, blocks, and the blockchain, and the second structure models as well maturation time for coinbase transactions and Merkle trees. Hashing and cryptographic operations and their correctness are dealt with abstractly by postulating corresponding operations. An indication is given how the correctness of this model could be specified and proven in Agda.
Claude Crépeau, Nan Yang
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.
Claude Crépeau, Nan Yang
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.
Yupeng Zhang
We study the problem of argument systems, where a computationally weak verifier outsources the execution of a computation to a powerful but untrusted prover, while being able to validate that the result was computed correctly through a proof generated by the prover. In addition, the zero-knowledge property guarantees that proof leaks no information about the potential secret input from the prover. Existing efficient zero-knowledge arguments with sublinear verification time require an expensive preprocessing phase that depends on a particular computation, and incur big overhead on the prover time and prover memory consumption. This thesis proposes new constructions for zero-knowledge arguments that overcome the above problems. The new constructions require only a one time preprocessing and can be used to validate any computations later. They also reduce the overhead on the prover time and memory by orders of magnitude. We apply our new constructions to build a verifiable database system and verifiable RAM programs, leading to significant improvements over prior work.
Damiano Azzolini, Fabrizio Riguzzi, Evelina Lamma, Elena Bellodi · 5 authors
Bitcoin is one of the first decentralized, peer to peer, payment systems based on the so-called Proof-of-Work (PoW). PoW is an algorithm that requires the computation of a hard function in order to gain access to a resource but, at the same time, the correctness of the computed result should be easily checked. The use of a PoW removes the necessity of a centralized third party and so the consistency of the network may be altered directly by the involved users. Peers, to solve the PoW more efficiently, usually organize themselves into mining pools, to increase the overall computational power: this situation, unfortunately, leads to a network centralization. In this paper we consider two typical scenarios of a Bitcoin network and we model them by probabilistic logic programming (PLP): the centralization of the hashing power by large pools and the “double spending attack”. In the first one, we verify the effectiveness of a protocol that attempts to discourage the formation of large pools. In the second one, we compute the probability of success of an attacker. Both scenarios are modeled using the PLP package cplint.
Kai Brünnler, Dandolo Flumini, Thomas Studer
Abstract Blockchains are distributed data structures that are used to achieve consensus in systems for cryptocurrencies (like Bitcoin) or smart contracts (like Ethereum). Although blockchains gained a lot of popularity recently, there are only few logic-based models for blockchains available. We introduce $\mathsf{BCL}$, a dynamic logic to reason about blockchain updates, and show that $\mathsf{BCL}$ is sound and complete with respect to a simple blockchain model.
Dr Craig S Wright
We demonstrate that the Bitcoin Script language allows not only for primitive recursion, but in the deployment of an Ackerman function and hence the ability to simply recurse in Bitcoin script, we show that the script system is Turing complete. From this, we introduce a new class of Turing Machine, the PTTM or probabilistic Total Turing machine and note that Bitcoin acts as a decider or Total Turing Machine which allows us to find a NIZKPoK that can act as a TM based verifier to a Non-Interactive Proof that is run on an external and non-associated TM as a proof system. Bitcoin can extend to securely offer contracts such as best fit solutions to common logistic systems and optimisation problems including the Travelling Salesman class of problems and to the optimisation of systems. This can be offered as an open or time bound contract that guarantees payment and can be solved which allowing Pseudonymity of the bidder.
Itay Berman, Ron D. Rothblum, Vinod Vaikuntanathan
© Itay Berman, Ron D. Rothblum and Vinod Vaikuntanathan. Interactive proofs of proximity (IPPs) are interactive proofs in which the verifier runs in time sub-linear in the input length. Since the verifier cannot even read the entire input, following the property testing literature, we only require that the verifier reject inputs that are far from the language (and, as usual, accept inputs that are in the language). In this work, we initiate the study of zero-knowledge proofs of proximity (ZKPP). A ZKPP convinces a sub-linear time verifier that the input is close to the language (similarly to an IPP) while simultaneously guaranteeing a natural zero-knowledge property. Specifically, the verifier learns nothing beyond (1) the fact that the input is in the language, and (2) what it could additionally infer by reading a few bits of the input. Our main focus is the setting of statistical zero-knowledge where we show that the following hold unconditionally (where N denotes the input length): Statistical ZKPPs can be sub-exponentially more efficient than property testers (or even non-interactive IPPs): We show a natural property which has a statistical ZKPP with a polylog(N) time verifier, but requires (N) queries (and hence also runtime) for every property tester. Statistical ZKPPs can be sub-exponentially less efficient than IPPs: We show a property which has an IPP with a polylog(N) time verifier, but cannot have a statistical ZKPP with even an No(1) time verifier. Statistical ZKPPs for some graph-based properties such as promise versions of expansion and bipartiteness, in the bounded degree graph model, with polylog(N) time verifiers exist. Lastly, we also consider the computational setting where we show that: Assuming the existence of one-way functions, every language computable either in (logspace uniform) NC or in SC, has a computational ZKPP with a (roughly) N time verifier. Assuming the existence of collision-resistant hash functions, every language in NP has a statistical zero-knowledge argument of proximity with a polylog(N) time verifier.
Thomas Vidick, John Watrous
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*.
Juan A. Garay
Distributed consensus (aka Byzantine agreement [Pease, Shostak & Lamport, 1980]) is one of the fundamental problems in fault-tolerant distributed computing and cryptographic protocols. It requires correct participants (parties) to reach agreement on initially held values despite the arbitrary behavior of some of them, with the additional requirement (known as Validity) that if all the correct participants start off with the same value, then that must be the decision value. The problem has been studied extensively in both the unconditional setting (where no assumptions are made about the computational power of the adversary) and the cryptographic setting, and efficient (i.e., polynomial-time) solutions exist tolerating the optimal number of misbehaving parties and running in the optimal number of rounds, on networks with pairwise authenticated channels. In many interesting scenarios, however, such as "peer-to-peer" networks, where parties come and go as they please and there are no prior relations among them, such infrastructure (pairwise authenticated channels, public-key infrastructure) is unavailable, thus raising the question whether anything "interesting" can be achieved. In this talk we answer this question in the affirmative, presenting two new probabilistic consensus protocols based on "proofs of work" (POWs, aka "moderately hard functions," "cryptographic puzzles" [Dwork & Naor, 1992]), the technology underlying Bitcoin, the first and most popular decentralized cryptocurrency to date. (In Bitcoin, POWs are implemented using the SHA-256 cryptographic hash function, by finding preimages that produce values in a given smaller domain.) In more detail, we first extract and analyze the core of the Bitcoin protocol, which we term the Bitcoin backbone, and prove two fundamental properties of its "blockchain" approach which we call "common prefix" and "chain quality." The consensus protocols can then be built as applications on top of the backbone protocol, with the Agreement and Validity properties following from common prefix and chain quality, respectively. The first protocol works assuming the adversary's hashing power is bounded by 1/3 of the network's total hashing power. The second consensus protocol is more elaborate, relies on the notion of robust transaction ledgers, which capture the essence of Bitcoin's operation as a cryptocurrency, and works assuming the adversary's hashing power is strictly less than 1/2.
George Danezis, Cédric Fournet, Jens Groth, Markulf Kohlweiss
No abstract is available for this record.
Salvador Lucas, José Meseguer
No abstract is available for this record.
Nan Yang
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.
Jannik Dreier, Guillaume Dumas, Hugo Jonker, Pascal Lafourcade
An electronic auction protocol will only be used by those who trust that it operates correctly. Therefore, e-auction protocols must be verifiable: seller, buyer and losing bidders must all be able to determine that the result was correct. We pose that the importance of verifiability for e-auctions necessitates a formal analysis. Consequently, in the first part of the talk, we identify notions of verifiability for each stakeholder. We formalize these and then use the developed framework to study the verifiability of several examples. We provide an analysis of the protocol by Sako in the applied pi-calculus with help of ProVerif, finding it to be correct. Additionally we identify issues with the protocols due to Curtis et al. and Brandt. In the second part, we will analyze the protocol by Brandt in more detail. We show first that this protocol – when using malleable interactive zero-knowledge proofs – is vulnerable to attacks by dishonest bidders. Such bidders can manipulate the publicly available data in a way that allows the seller to deduce all participants’ bids. Additionally we discuss attacks on non-repudiation, fairness and the privacy of individual bidders exploiting authentication problems.
Estefanía Argente, Olivier Boissier, Carlos Carrascosa, Nicoletta Fornara · 13 authors
The notion of Multi-Agent System (MAS) environment, as remarked by recent literature, has gained a key role, becoming a mediating entity, functioning as enabler but possibly also as a manager and constrainer of agent actions, perceptions, and interactions 1 while addressing the requirements of openness and scalability. According to such a perspective, the environment is not a merely passive source of agent perceptions and target of agent actions which is, actually, the dominant perspective in agency, but a first-class abstraction that can be suitably designed to encapsulate some fundamental functionalities and services, such as coordination and organization, besides agent mobility, communications, security, etc [2]. Then, the environment dimension appears to intersect with all the dimensions that should be addressed to define an agreement between autonomous agents, that is, all the different Agreement Technologies giving support to the building, development and management of agreements in decentralized and open systems between autonomous agents. Those dimensions are the ones related to the development of technologies dealing with: Semantics, Norms, Organizations, Argumentation & Negotiation, and Trust.
Salil Vadhan, Shafi Goldwasser
Thesis (Ph.D.)--Massachusetts Institute of Technology, Dept. of Mathematics, 1999.
Shlomi Dolev, Panagiota N. Panagopoulou, Mikaël Rabie, Elad M. Schiller · 5 authors
Players in a game are assumed to be totally rational and absolutely smart. However, in reality all players may act in non-rational ways and may fail to understand and find their best actions. In particular, participants in social interactions, such as lotteries and auctions, cannot be expected to always find by themselves the "best-reply" to any situation. Indeed, agents may consult with others about the possible outcome of their actions. It is then up to the counselee to assure the rationality of the consultant's advice. We present a distributed computer system infrastructure, named rationality authority, that allows safe consultation among (possibly biased) parties. The parties' advices are adapted only after verifying their feasibility and optimality by standard formal proof checkers. The rationality authority design considers computational constraints, as well as privacy and security issues, such as verification methods that do not reveal private preferences. Some of the techniques resembles zero-knowledge proofs. A non-cooperative game is presented by the game inventor along with its (possibly intractable) equilibrium. The game inventor advises playing by this equilibrium and offers a checkable proof for the equilibrium feasibility and optimality. Standard verification procedures, provided by trusted (according to their reputation) verification procedures, are used to verify the proof. Thus, the proposed rationality authority infrastructure facilitates the applications of game theory in several important real-life scenarios by the use of computing systems.