An official website of the United States government
We present gOTzilla, a protocol for interactive zero-knowledge proofs for very large disjunctive statements of the following format: given publicly known circuit C, and set of values Y = {y1 , . . . , yn }, prove knowledge of a witness x such that C(x) = y1 ∨ C(x) = y2 ∨ · · · ∨ C(x) = yn . These type of statements are extremely important for the proof of assets (PoA) problem in cryptocurrencies where a prover wants to prove the knowledge of a secret key sk that associates with the hash of a public key H(pk) posted on the ledger. We note that the size of n in popular cryptocurrencies, such as Bitcoin, is estimated to 80 million. For the construction of gOTzilla, we start by observing that if we restructure the proof statement to an equivalent of proving knowledge of (x, y) such that (C(x) = y) ∧ (y = y1 ∨ · · · ∨ y = yn )), then we can reduce the disjunction of equalities to 1-out-of-N oblivious transfer (OT). Our overall protocol is based on the MPC in the head (MPCitH) paradigm. We additionally provide a concrete, efficient extension of our protocol for the case where C combines algebraic and non-algebraic statements (which is the case in the PoA application). We achieve an asymptotic communication cost of O(log n) plus the proof size of the underlying MPCitH protocol. While related work has similar asymptotic complexity, our approach results in concrete performance improvements. We implement our protocol and provide benchmarks. Concretely, for a set of size 1 million entries, the total run-time of our protocol is 14.89 seconds using 48 threads, with 6.18 MB total communication, which is about 4x faster compared to the state of the art when considering a disjunctive statement with algebraic and non-algebraic elements.
more »
« less
Short Paper: The Proof is in the Pudding: Proofs of Work for Solving Discrete Logarithms
We propose a proof of work protocol that computes the discrete logarithm of an element in a cyclic group. Individual provers generating proofs of work perform a distributed version of the Pollard rho algorithm. Such a protocol could capture the computational power expended to construct proof-of-work-based blockchains for a more useful purpose, as well as incentivize advances in hardware, software, or algorithms for an important cryptographic problem. We describe our proposed construction and elaborate on challenges and potential trade-offs that arise in designing a practical proof of work.
more »
« less
- Award ID(s):
- 1651344
- PAR ID:
- 10174440
- Date Published:
- Journal Name:
- FC 2019: Financial Cryptography and Data Security
- Page Range / eLocation ID:
- 396-404
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Proving the correctness of a distributed protocol is a challenging endeavor. Central to this task is finding an inductive invariant for the protocol. Currently, automated invariant inference algorithms require developers to describe protocols using a restricted logic. If the developer wants to prove a protocol expressed without these restrictions, they must devise an inductive invariant manually. We propose an approach that simplifies and partially automates finding the inductive invariant of a distributed protocol, as well as proving that it really is an invariant. The key insight is to identify an invariant taxonomy that divides invariants into Regular Invariants, which have one of a few simple low-level structures, and Protocol Invariants, which capture the higher-level host relationships that make the protocol work. Building on the insight of this taxonomy, we describe the Kondo methodology for proving the correctness of a distributed protocol modeled as a state machine. The developer first manually devises the Protocol Invariants by proving a synchronous version of the protocol correct. In this simpler version, sends and receives are replaced with atomic variable assignments. The Kondo tool then automatically generates the asynchronous protocol description, Regular Invariants, and proofs that the Regular Invariants are inductive on their own. Finally, Kondo combines these with the synchronous proof into a draft proof of the asynchronous protocol, which may then require a small amount of user effort to complete. Our evaluation shows that Kondo reduces developer effort for a wide variety of distributed protocols.more » « less
-
Distributed systems are notoriously difficult to design and implement correctly. Formal verification provides correctness proofs, and has recently been successfully applied to various distributed systems. At the heart of a typical formal verification is a computer-checked proof with an inductive invariant. Finding this inductive invariant is the hardest part of the proof: a part that is currently undertaken manually by the developer and is responsible for most of the effort associated with formal verification. In this paper, we present a new approach: Incremental Inference of Inductive Invariants (I4), to automatically generate inductive invariants for distributed protocols. We start from a simple idea: the inductive invariant of a finite instance of the protocol must be an instance of a general inductive invariant for the infinite distributed protocol. In I4, we instantiate a finite instance of the protocol, work out the finite inductive invariant of this instance, then figure out the general inductive invariant as a generalization of the finite invariant. Our experiments show that I4 can finish the general proof of correctness of several systems with minimal human effort.more » « less
-
In this work, we propose a blockchain-based solution for securing robot-to-robot communication for a task with a high socioeconomic impact—information gathering. The objective of the robots is to gather maximal information about an unknown ambient phenomenon such as soil humidity distribution in a field. More specifically, we use the proof-of-work (PoW) consensus protocol for the robots to securely coordinate while rejecting tampered data injected by a malicious entity. As the blockchain-based PoW protocol has a large energy footprint, we next employ an algorithmically-engineered energy-efficient version of PoW. Results show that our proposed energy-efficient PoW-based protocol can reduce energy consumption by 14% while easily scaling up to 10 robots.more » « less
-
We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and implemented in MongoDB, a distributed database whose replication protocol is derived from the Raft consensus algorithm. We present an inductive invariant for MongoRaftReconfig that is formalized in TLA+ and formally proved using the TLA+ proof system (TLAPS). We also present a formal TLAPS proof of two key safety properties of MongoRaftReconfig, LeaderCompleteness and StateMachineSafety. To our knowledge, these are the first machine checked inductive invariant and safety proof of a dynamic reconfiguration protocol for a Raft based replication system.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1007/978-3-030-32101-7_24
