Modeling and verification of the Bitcoin protocol

Kaylash Chaudhary; Ansgar Fehnker; Jaco van de Pol; Mariëlle Stoelinga

doi:10.4204/EPTCS.196.5

Modeling and verification of the Bitcoin protocol

Kaylash Chaudhary, Ansgar Fehnker, Jaco van de Pol, Mariëlle Stoelinga

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

20 Citations (Scopus)

27 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 language	English
Title of host publication	Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015)
Editors	Rob van Glabbeek, Jan Friso Groote, Peter Höfner
Place of Publication	Waterloo, NSW
Publisher	Open Publishing Association
Pages	46-60
Number of pages	15
DOIs	https://doi.org/10.4204/EPTCS.196.5
Publication status	Published - 2015
Externally published	Yes
Event	1st Workshop on Models for Formal Analysis of Real Systems, MARS 2015 - Suva, Fiji Duration: 23 Nov 2015 → 23 Nov 2015

Publication series

Name	Electronic Proceedings in Theoretical Computer Science
Publisher	Open Publishing Association
Volume	196

Conference

Conference	1st Workshop on Models for Formal Analysis of Real Systems, MARS 2015
Country/Territory	Fiji
City	Suva
Period	23/11/15 → 23/11/15

Bibliographical note

Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

Keywords

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

Access to Document

10.4204/EPTCS.196.5

Publisher version (open access)Final published version, 653 KBLicence: CC BY

http://eptcs.web.cse.unsw.edu.au/paper.cgi?MARS2015.5

Cite this

Chaudhary, K., Fehnker, A., van de Pol, J., & Stoelinga, M. (2015). Modeling and verification of the Bitcoin protocol. In R. 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). Open Publishing Association. https://doi.org/10.4204/EPTCS.196.5

Chaudhary, Kaylash ; Fehnker, Ansgar ; van de Pol, Jaco et al. / Modeling and verification of the Bitcoin protocol. Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015). editor / Rob van Glabbeek ; Jan Friso Groote ; Peter Höfner. Waterloo, NSW : Open Publishing Association, 2015. pp. 46-60 (Electronic Proceedings in Theoretical Computer Science).

@inproceedings{479d20d9c60849fe88d23ab00d05c5e1,

title = "Modeling and verification of the Bitcoin protocol",

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.",

keywords = "FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS, EWI-26442, IR-98391, Block-chain, METIS-315020, Bitcoin",

author = "Kaylash Chaudhary and Ansgar Fehnker and {van de Pol}, Jaco and Mari{\"e}lle Stoelinga",

note = "Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.; 1st Workshop on Models for Formal Analysis of Real Systems, MARS 2015 ; Conference date: 23-11-2015 Through 23-11-2015",

year = "2015",

doi = "10.4204/EPTCS.196.5",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "Open Publishing Association",

pages = "46--60",

editor = "{van Glabbeek}, Rob and Groote, {Jan Friso} and Peter H{\"o}fner",

booktitle = "Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015)",

}

Chaudhary, K, Fehnker, A, van de Pol, J & Stoelinga, M 2015, Modeling and verification of the Bitcoin protocol. in R van Glabbeek, JF Groote & P Höfner (eds), Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015). Electronic Proceedings in Theoretical Computer Science, vol. 196, Open Publishing Association, Waterloo, NSW, pp. 46-60, 1st Workshop on Models for Formal Analysis of Real Systems, MARS 2015, Suva, Fiji, 23/11/15. https://doi.org/10.4204/EPTCS.196.5

Modeling and verification of the Bitcoin protocol. / Chaudhary, Kaylash; Fehnker, Ansgar; van de Pol, Jaco et al.
Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015). ed. / Rob van Glabbeek; Jan Friso Groote; Peter Höfner. Waterloo, NSW: Open Publishing Association, 2015. p. 46-60 (Electronic Proceedings in Theoretical Computer Science; Vol. 196).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Modeling and verification of the Bitcoin protocol

AU - Chaudhary, Kaylash

AU - Fehnker, Ansgar

AU - van de Pol, Jaco

AU - Stoelinga, Mariëlle

N1 - Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

KW - EWI-26442

KW - IR-98391

KW - Block-chain

KW - METIS-315020

KW - Bitcoin

U2 - 10.4204/EPTCS.196.5

DO - 10.4204/EPTCS.196.5

M3 - Conference proceeding contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 46

EP - 60

BT - Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015)

A2 - van Glabbeek, Rob

A2 - Groote, Jan Friso

A2 - Höfner, Peter

PB - Open Publishing Association

CY - Waterloo, NSW

T2 - 1st Workshop on Models for Formal Analysis of Real Systems, MARS 2015

Y2 - 23 November 2015 through 23 November 2015

ER -

Chaudhary K, Fehnker A, van de Pol J, Stoelinga M. Modeling and verification of the Bitcoin protocol. In van Glabbeek R, Groote JF, Höfner P, editors, Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015). Waterloo, NSW: Open Publishing Association. 2015. p. 46-60. (Electronic Proceedings in Theoretical Computer Science). doi: 10.4204/EPTCS.196.5

Modeling and verification of the Bitcoin protocol

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Fingerprint

Cite this