Provably Secure Blockchains


August 2016 – December 2018.


Christian Badertscher (ETH Zurich)
Ueli Maurer (ETH Zurich)
Daniel Tschudi (Aarhus University)
Vassilis Zikas (University of Edinburgh)
Juan Garay (Texas A&M University)


This project aims to analyze the security of blockchain protocols from a provable security point of view. In a first phase, the goal is to formalize Bitcoin’s ultimate goal as a ledger functionality in a universally composable language and to show that this functionality is securely realized by an appropriate abstraction of the Bitcoin protocol. The goal is to propose a ledger functionality that is general enough such that it can be realized also by other concrete blockchain protocols, hence becoming the standard security goal for blockchains in general. More specifically, we put forth a universally composable treatment of the Bitcoin protocol. We specify the goal that Bitcoin aims to achieve as a ledger functionality in the (G)UC model of Canetti et al. [TCC’07]. Our ledger functionality is weaker than the one recently proposed by Kiayias, Zhou, and Zikas [EUROCRYPT’16], but unlike the latter suggestion, which is arguably not implementable given the Bitcoin assumptions, we prove that the one proposed here is securely UC realized under standard assumptions by an appropriate abstraction of Bitcoin as a UC protocol.

In a second phase, the projects tries to challenge the assumptions behind the security proof. While the famous assumptions that the majority of the mining power is honest is widely accepted, the aim of this project is to investigate alternative assumptions such as rational assumptions on miners’ incentives. In addition, the project tries to minimize assumptions, for example reducing the amount of synchrony that the protocols and the proofs rely on. We employ the machinery from the Rational Protocol Design (RPD) framework by Garay et al. [FOCS’13]. We show assuming a natural class of incentives for the miners’ behavior (i.e., rewarding them for adding blocks to the blockchain but having them pay for mining), where one can reserve the honest majority assumption as a fallback, or even, depending on the application, completely replace it by the assumption that the miners aim to maximize their revenue. Our results underscore the appropriateness of RPD as a “rational cryptography” framework for analyzing Bitcoin. long the way, we devise significant extensions to the original RPD machinery that broaden its applicability to cryptocurrencies, which may be of independent interest.


Bitcoin as a Transaction Ledger: A Composable Treatment.
C. Badertscher, U. Maurer, D. Tschudi, V. Zikas.
Advances in Cryptology – CRYPTO 2017 – Proceedings, Part I, pp. 324-356, 2017.

But Why Does it Work? A Rational Protocol Design Treatment of Bitcoin.
C. Badertscher, J. Garay, U. Maurer, D. Tschudi, V. Zikas.
Advances in Cryptology – EUROCRYPT 2018 – Proceedings, Part II, pp. 34-65, 2018.