Modeling and Verification of the Bitcoin Protocol

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    6 Citations (Scopus)
    346 Downloads (Pure)

    Abstract

    Bitcoin is a popular digital currency for online payments, realized as a decentralized peer-to-peer electronic cash system. Bitcoin keeps a ledger of all transactions; the majority of the participants decides on the correct ledger. Since there is no trusted third party to guard against double spending, and inspired by its popularity, we would like to investigate the correctness of the Bitcoin protocol. Double spending is an important threat to electronic payment systems. Double spending would happen if one user could force a majority to believe that a ledger without his previous payment is the correct one. We are interested in the probability of success of such a double spending attack, which is linked to the computational power of the attacker. This paper examines the Bitcoin protocol and provides its formalization as an UPPAAL model. The model will be used to show how double spending can be done if the parties in the Bitcoin protocol behave maliciously, and with what probability double spending occurs.
    Original languageEnglish
    Title of host publicationProceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015)
    EditorsR.J. van Glabbeek, J.F. Groote, P. Höfner
    Place of PublicationAustralia
    PublisherOpen Publishing Association
    Pages46-60
    Number of pages15
    DOIs
    Publication statusPublished - 13 Nov 2015

    Publication series

    NameElectronic Proceedings in Theoretical Computer Science
    PublisherOpen Publishing Association
    Volume196
    ISSN (Print)2075-2180
    ISSN (Electronic)2075-2180

    Keywords

    • FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS
    • EWI-26442
    • IR-98391
    • Block-chain
    • METIS-315020
    • Bitcoin

    Fingerprint Dive into the research topics of 'Modeling and Verification of the Bitcoin Protocol'. Together they form a unique fingerprint.

  • Cite this

    Chaudhary, K., Fehnker, A., van de Pol, J. C., & Stoelinga, M. I. A. (2015). Modeling and Verification of the Bitcoin Protocol. In R. J. van Glabbeek, J. F. Groote, & P. Höfner (Eds.), Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015) (pp. 46-60). (Electronic Proceedings in Theoretical Computer Science; Vol. 196). Australia: Open Publishing Association. https://doi.org/10.4204/EPTCS.196.5