Modeling and Verification of the Bitcoin Protocol

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

    8 Citations (Scopus)
    457 Downloads (Pure)


    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
    Number of pages15
    Publication statusPublished - 13 Nov 2015
    EventWorkshop on Models for Formal Analysis of Real Systems, MARS 2015 - Suva, Fiji
    Duration: 23 Nov 201523 Nov 2015

    Publication series

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


    WorkshopWorkshop on Models for Formal Analysis of Real Systems, MARS 2015
    Other23 November 2015


    • 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