We propose and study a new class of polynomial voting rules for a general decentralized decision/consensus system, and more specifically for the proof-of-stake protocol. The main idea, inspired by the Penrose square-root law and the more recent quadratic voting rule, is to differentiate a voter’s voting power and the voter’s share (fraction of the total in the system). We show that, whereas voter shares form a martingale process that converges to a Dirichlet distribution, their voting powers follow a supermartingale process that decays to zero over time. This prevents any voter from controlling the voting process and, thus, enhances security. For both limiting results, we also provide explicit rates of convergence. When the initial total volume of votes (or stakes) is large, we show a phase transition in share stability (or the lack thereof), corresponding to the voter’s initial share relative to the total. We also study the scenario in which trading (of votes/stakes) among the voters is allowed and quantify the level of risk sensitivity (or risk aversion) in three categories, corresponding to the voter’s utility being a supermartingale, a submartingale, and a martingale. For each category, we identify the voter’s best strategy in terms of participation and trading. Funding: W. Tang gratefully acknowledges financial support through the National Science Foundation [Grants DMS-2113779 and DMS-2206038] and through a start-up grant at Columbia University. D. D. Yao’s work is part of a Columbia–City University/Hong Kong collaborative project that is supported by InnoHK Initiative, the Government of Hong Kong Special Administrative Region, and the Laboratory for AI-Powered Financial Technologies.
Peg solitaire is a very popular traditional single-player board game, known to be NP-complete. In this paper, we present a zero-knowledge proof of knowledge for solutions of peg solitaire instances. Our proof is straightforward, in the sense that it does not use any reduction to another NP-complete problem, and uses the standard design of sigma protocols. Our construction relies on cryptographic commitments, which can be replaced by envelopes to make the protocol physical. As a side contribution, we introduce the notion of isomorphisms for peg solitaire, which is the key tool of our protocol.
Abstract We use a simplified version of the framework of resource monoids , introduced by Dal Lago and Hofmann, to interpret simply typed λ-calculus with constants zero and successor. We then use this model to prove a simple quantitative result about bounding the size of the normal form of λ-terms. While the bound itself is already known, this is to our knowledge the first semantic proof of this fact. Our use of resource monoids differs from the other instances found in the literature, in that it measures the size of λ-terms rather than time complexity.
A key component of blockchain technology is the ledger, viz., a database\nthat, unlike standard databases, keeps in memory the complete history of past\ntransactions as in a notarial archive for the benefit of any future test. In\nsecond-generation blockchains such as Ethereum the ledger is coupled with smart\ncontracts, which enable the automation of transactions associated with\nagreements between the parties of a financial or commercial nature. The\ncoupling of smart contracts and ledgers provides the technological background\nfor very innovative application areas, such as Decentralized Autonomous\nOrganizations (DAOs), Initial Coin Offerings (ICOs) and Decentralized Finance\n(DeFi), which propelled blockchains beyond cryptocurrencies that were the only\nfocus of first generation blockchains such as the Bitcoin. However, the\ncurrently used implementation of smart contracts as arbitrary programming\nconstructs has made them susceptible to dangerous bugs that can be exploited\nmaliciously and has moved their semantics away from that of legal contracts. We\npropose here to recompose the split and recover the reliability of databases by\nformalizing a notion of contract modelled as a finite-state automaton with\nwell-defined computational characteristics derived from an encoding in terms of\nallocations of resources to actors, as an alternative to the approach based on\nprogramming. To complete the work, we use temporal logic as the basis for an\nabstract query language that is effectively suited to the historical nature of\nthe information kept in the ledger.\n
A key component of blockchain technology is the ledger, viz., a database that, unlike standard databases, keeps in memory the complete history of past transactions as in a notarial archive for the benefit of any future test. In second-generation blockchains such as Ethereum the ledger is coupled with smart contracts, which enable the automation of transactions associated with agreements between the parties of a financial or commercial nature. The coupling of smart contracts and ledgers provides the technological background for very innovative application areas, such as Decentralized Autonomous Organizations (DAOs), Initial Coin Offerings (ICOs) and Decentralized Finance (DeFi), which propelled blockchains beyond cryptocurrencies that were the only focus of first generation blockchains such as the Bitcoin. However, the currently used implementation of smart contracts as arbitrary programming constructs has made them susceptible to dangerous bugs that can be exploited maliciously and has moved their semantics away from that of legal contracts. We propose here to recompose the split and recover the reliability of databases by formalizing a notion of contract modelled as a finite-state automaton with well-defined computational characteristics derived from an encoding in terms of allocations of resources to actors, as an alternative to the approach based on programming. To complete the work, we use temporal logic as the basis for an abstract query language that is effectively suited to the historical nature of the information kept in the ledger.
Abstract We introduce the probabilistic two-agent justification logic $\textsf {IPJ}$, a logic in which we can reason about agents that perform interactive proofs. In order to study the growth rate of the probabilities in $\textsf {IPJ}$, we present a new method of parametrizing $\textsf {IPJ}$ over certain negligible functions. Further, our approach leads to a new notion of zero-knowledge proofs.
Attribute-based cryptography becomes one of the hot topics in cryptography, since it can provide fine-grained access control and good privacy. Σ-protocol is a 3-move public-coin honest verifier zero-knowledge proof protocol, and has important applications in many fields of cryptography. Firstly, combining the concept of attribute-based cryptography with the zero-knowledge proof, a notion of attribute-based Σ-protocol is introduced with its formal security model. Secondly, based on the standard Σ-protocol, the trapdoor samplable relation and the smooth secret sharing, a general construction of decentralized attribute-based Σ-protocol and corresponding scheme are proposed with the proofs of its securities. Finally, as the applications of decentralized attribute-based Σ-protocol, general constructions of decentralized attribute-based signature and decentralized attribute-based two-tier signature are presented by Fiat-Shamir transformation, respectively. Some concrete schemes are also presented. Performance analysis shows that the proposed attribute-based two-tier signature scheme has obvious advantages in both sizes and computation costs compared with existing schemes.
This paper investigates the usage of logic and logic programming in the design of smart contracts. Our starting point is the logic-based programming language for smart contracts used in a recently proposed framework of quantum-secured blockchain, called Logicontract (LC). We then extend the logic used in LC by answer set programming (ASP), a modern approach to declarative logic programming. Using ASP enables us to write various interesting smart contracts, such as conditional payment, commitment, multi-party lottery and legal service. A striking feature of our ASP implementation proposal is that it involves post-quantum cryptographic primitives, such as the lattice-based public key encryption and signature. The adoption of the post-quantum cryptographic signature overcomes a specific limitation of LC in which the unconditionally secure signature, despite its strength, offers limited protection for users of the same node.
In critical systems, failures or errors can cause catastrophes, such as deaths or considerably losses of money. Model checking provides an automated way to prove the correctness of programs' requirements. It is a convenient technique to use in systems that need reliability. Propositional Dynamic Logic (PDL) is a formal system designed to reason about programs. This work presents a compiler implementation from a subset of the C language and also for the Smacco model, both to the PDL language, and after that to the language of the nuXmv model checker. This implementation is linked with a Blockchain model generation system to model and reason about smart contracts.
Elliptic curves with a bilinear map, or pairing, have a rich algebraic structure that has been fundamental to develop practical Non-Interactive Zero-Knowledge (NIZK) proofs. On the theoretical side, we explore how efficient can NIZK proofs be under weak complexity assumptions. Specifically, we reduce the cost of proofs of satisfiability of quadratic equations, we define a new commitment scheme that is compatible with other pairing-based NIZK arguments, and we construct a simulation-sound argument that results in a new a signature of knowledge with communication sublinear in the circuit size under standard assumptions. Additionally, we study how to reduce the cost of verification in one of the most widely deployed NIZK arguments in practice.
Modern mathematics is built on the idea that proofs should be translatable\ninto formal proofs, whose validity is an objective question, decidable by a\ncomputer. Yet, in practice, proofs are informal and may omit many details. An\nagent considers a proof valid if they trust that it could be expanded into a\nmachine-verifiable proof. A proof's validity can thus become a subjective\nmatter and lead to a debate, which may be difficult to settle. Hence, while the\nconcept of valid proof is well-defined, the process to establish validity is\nitself a complex multi-agent problem.\n We introduce the SPRIG protocol. SPRIG allows agents to propose and verify\nsuccinct and informative proofs in a decentralized fashion; the trust is\nestablished by agents being able to request more details in the proof steps;\ndebates, if they arise, must isolate details of proofs and, if they persist, go\ndown to machine-level details, where they are automatically settled. A\nstructure of bounties and stakes is set to incentivize agents to act in good\nfaith.\n We propose a game-theoretic discussion of SPRIG, showing how agents with\nvarious types of information interact, leading to a proof tree with an\nappropriate level of detail and to the invalidation of wrong proofs, and we\ndiscuss resilience against various attacks. We then analyze a simplified model,\ncharacterize its equilibria and compute the agents' level of trust.\n SPRIG is designed to run as a smart contract on a blockchain platform. This\nallows anonymous agents to participate in the verification debate, and to\ncontribute with their information. The smart contract mediates the\ninteractions, settles debates, and guarantees that bounties and stakes are paid\nas specified.\n SPRIG enables new applications, such as the issuance of bounties for open\nproblems, and the creation of derivatives markets, allowing agents to inject\nmore information pertaining to proofs.\n
We show a lattice-based solution for commit-and-prove transparent circuit zero-knowledge (ZK) with polylog-communication, the first not depending on PCPs. We start from compressed Σ-protocol theory (CRYPTO 2020), which is built around basic Σ-protocols for opening an arbitrary linear form on a long secret vector that is compactly committed to. These protocols are first compressed using a recursive “folding-technique” adapted from Bulletproofs, at the expense of logarithmic rounds. Proving in ZK that the secret vector satisfies a given constraint – captured by a circuit – is then by (blackbox) reduction to the linear case, via arithmetic secret-sharing techniques adapted from MPC. Commit-and-prove is also facilitated, i.e., when commitment(s) to the secret vector are created ahead of any circuit-ZK proof. On several platforms (incl. DL) this leads to logarithmic communication. Non-interactive versions follow from Fiat-Shamir. This abstract modular theory strongly suggests that it should somehow be supported by a lattice platform as well. However, when going through the motions and trying to establish low communication (on an SIS-platform), a certain significant lack in current understanding of multi-round protocols is exposed. Namely, as opposed to the DL-case, the basic Σ-protocol in question typically has poly-small challenge space. Taking into account the compression-step – which yields non-constant rounds – and the necessity for parallelization to reduce error, there is no known tight result that the compound protocol admits an efficient knowledge extractor. We resolve the state of affairs here by a combination of two novel results which are fully general and of independent interest. The first gives a tight analysis of efficient knowledge extraction in case of non-constant rounds combined with poly-small challenge space, whereas the second shows that parallel repetition indeed forces rapid decrease of knowledge error. Moreover, in our present context, arithmetic secret sharing is not defined over a large finite field but over a quotient of a number ring and this forces our careful adaptation of how the linearization techniques are deployed. We develop our protocols in an abstract framework that is conceptually simple and can be flexibly instantiated. In particular, the framework applies to arbitrary rings and norms.
Abstract A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This tool paper describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.
Sepehr Sharifi, Alireza Parvizimosaed, Daniel Amyot, Luigi Logrippo · 5 authors
Legal contracts specify the terms and conditions (in essence, requirements) that apply to business transactions. Smart contracts are software systems that monitor and control the execution of contracts to ensure compliance. This paper proposes a formal specification language for contracts, called Symboleo, where contracts consist of collections of obligations and powers that define the legal contract's compliant executions. The formal semantics of Symboleo is based on an extension of an ontology for Law and is described in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations and powers. Our proposal includes a preliminary evaluation through the specification of a real life-inspired Sale-of-Goods contract, with a prototype execution engine. We envision this language to enable formally verifying contracts to detect requirements-level issues and to generate executable smart contracts (e.g., on blockchain technology).
Abstract We condense the theory of UTxO blockchains down to a simple and compact set of four type equations (Idealised EUTxO), and to an algebraic characterisation (abstract chunk systems), and exhibit an adjoint pair of functors between them. This gives a novel account of the essential mathematical structures underlying blockchain technology, such as Bitcoin.
Many important cryptographic primitives offer probabilistic guarantees of\nsecurity that can be specified as quantitative hyperproperties; these are\nspecifications that stipulate the existence of a certain number of traces in\nthe system satisfying certain constraints. Verification of such hyperproperties\nis extremely challenging because they involve simultaneous reasoning about an\nunbounded number of different traces. In this paper, we introduce a technique\nfor verification of quantitative hyperproperties based on the notion of trace\nenumeration relations. These relations allow us to reduce the problem of\ntrace-counting into one of model-counting of formulas in first-order logic. We\nalso introduce a set of inference rules for machine-checked reasoning about the\nnumber of satisfying solutions to first-order formulas (aka model counting).\nPutting these two components together enables semi-automated verification of\nquantitative hyperproperties on infinite state systems. We use our methodology\nto prove confidentiality of access patterns in Path ORAMs of unbounded size,\nsoundness of a simple interactive zero-knowledge proof protocol as well as\nother applications of quantitative hyperproperties studied in past work.\n
Correct-by-Construction Casper (CBC Casper) is an Ethereum candidate consensus protocol undergoing active design and development. We present a formalization of CBC Casper using the Coq proof assistant that includes a model of the consensus protocol and proofs of safety and non-triviality protocol properties. We leverage Coq's type classes to model CBC Casper at various levels of abstraction. In doing so, we 1) illuminate the assumptions that each protocol property depends on, and 2) reformulate the protocol in general, mathematical terms. We highlight two advantages of our approach: 1) from a proof engineering perspective, it enables a clean separation of concerns between theory and implementation; 2) from a protocol engineering perspective, it provides a rigorous, foundational understanding of the protocol conducive to finding and proving stronger properties. We detail one such new property: strong non-triviality.
A key difference between using blockchains to store data and centrally controlled databases is that transactions are accepted to a blockchain via a consensus mechanism, and not by a controlling central party. Hence, once a user has issued a transaction, she cannot be certain if it will be accepted. Moreover, a yet unaccepted transaction cannot be retracted by the user, and may (or may not) be appended to the blockchain at any point in the future. This causes difficulties as the user may wish to formulate new transactions based on the knowledge of which previous transactions will be accepted. Yet this knowledge is inherently uncertain. We introduce a formal abstraction for blockchains as a data storage layer that underlies a database. The main issue that we tackle is the need to reason about possible worlds, due to the uncertainty in transaction appending. In particular, we consider the theoretical complexity of determining whether it is possible for a denial constraint to be contradicted, given the current state of the blockchain, pending transactions, and integrity constraints on blockchain data. We then present practical algorithms for this problem that work well in practice.
We present "Gasper," a proof-of-stake-based consensus protocol, which is an idealized version of the proposed Ethereum 2.0 beacon chain. The protocol combines Casper FFG, a finality tool, with LMD GHOST, a fork-choice rule. We prove safety, plausible liveness, and probabilistic liveness under different sets of assumptions.