Provable Security for Cryptocurrencies

The past several years have seen the surprising and rapid rise of Bitcoin and other “cryptocurrencies.” These are decentralized peer-to-peer networks that allow users to transmit money, tocompose financial instruments, and to enforce contracts between mutually distrusting peers, andthat show great promise as a foundation for financial infrastructure that is more robust, efficientand equitable than ours today. However, it is difficult to reason about the security of cryptocurrencies. Bitcoin is a complex system, comprising many intricate and subtly-interacting protocol layers. At each layer it features design innovations that (prior to our work) have not undergone any rigorous analysis. Compounding the challenge, Bitcoin is but one of hundreds of competing cryptocurrencies in an ecosystem that is constantly evolving. The goal of this thesis is to formally reason about the security of cryptocurrencies, reining in their complexity, and providing well-defined and justified statements of their guarantees. We provide a formal specification and construction for each layer of an abstract cryptocurrency protocol, and prove that our constructions satisfy their specifications. The contributions of this thesis are centered around two new abstractions: “scratch-off puzzles,” and the “blockchain functionality” model. Scratch-off puzzles are a generalization of the Bitcoin “mining” algorithm, its most iconic and novel design feature. We show how to provide secure upgrades to a cryptocurrency by instantiating the protocol with alternative puzzle schemes. We construct secure puzzles that address important and well-known challenges facing Bitcoin today, including wasted energy and dangerous coalitions. The blockchain functionality is a general-purpose model of a cryptocurrency rooted in the “Universal Composability” cryptography theory. We use this model to express a wide range of applications, including transparent “smart contracts” (like those featured in Bitcoin and Ethereum), and also privacy-preserving applications like sealed-bid auctions. We also construct a new protocol compiler, called Hawk, which translates user-provided specifications into privacy-preserving protocols based on zero-knowledge proofs.

EXISTENCE OF UNUSED MANAGED CAPACITY ON DEDICATED LANES AND AN ALTERNATIVE ON HOW TO SELL IT VIA AUCTIONS

This dissertation verifies whether the following two hypotheses are true: (1) High-occupancy/toll lanes (and therefore other dedicated lanes) have capacity that could still be used; (2) such unused capacity (or more precisely, “unused managed capacity”) can be sold successfully through a real-time auction. To show that the second statement is true, this dissertation proposes an auction-based metering (ABM) system, that is, a mechanism that regulates traffic that enters the dedicated lanes. Participation in the auction is voluntary and can be skipped by paying the toll or by not registering to the new system. This dissertation comprises the following four components: a measurement of unused managed capacity on an existing HOT facility, a game-theoretic model of an ABM system, an operational description of the ABM system, and a simulation-based evaluation of the system. Some other and more specific contributions of this dissertation include the following: (1) It provides a definition and a methodology for measuring unused managed capacity and another important variable referred as “potential volume increase”. (2) It proves that the game-theoretic model has a unique Bayesian Nash equilibrium. (3) And it provides a specific road design that can be applied or extended to other facilities. The results provide evidence that the hypotheses are true and suggest that the ABM system would benefit a public operator interested in reducing traffic congestion significantly, would benefit drivers when making low-reliability trips (such as work-to-home trips), and would potentially benefit a private operator interested in raising revenue.