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 languageUndefined
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
StatePublished - 13 Nov 2015

Publication series

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

Fingerprint

Electronic money

Keywords

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

Cite this

Chaudhary, K., Fehnker, A., 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. DOI: 10.4204/EPTCS.196.5

Chaudhary, Kaylash; Fehnker, Ansgar; Fehnker, Ansgar; van de Pol, Jan Cornelis; Stoelinga, Mariëlle Ida Antoinette / Modeling and Verification of the Bitcoin Protocol.

Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015). ed. / R.J. van Glabbeek; J.F. Groote; P. Höfner. Australia : Open Publishing Association, 2015. p. 46-60 (Electronic Proceedings in Theoretical Computer Science; Vol. 196).

Research output: Scientific - peer-reviewConference contribution

@inbook{0e13c33ec7ee41f9a0ff1f30cec4c2bd,
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 Ansgar Fehnker and {van de Pol}, {Jan Cornelis} and Stoelinga, {Mariëlle Ida Antoinette}",
note = "10.4204/EPTCS.196.5",
year = "2015",
month = "11",
doi = "10.4204/EPTCS.196.5",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "Open Publishing Association",
pages = "46--60",
editor = "{van Glabbeek}, R.J. and J.F. Groote and P. Höfner",
booktitle = "Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015)",

}

Chaudhary, K, Fehnker, A, Fehnker, A, van de Pol, JC & Stoelinga, MIA 2015, Modeling and Verification of the Bitcoin Protocol. in RJ 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, Australia, pp. 46-60. DOI: 10.4204/EPTCS.196.5

Modeling and Verification of the Bitcoin Protocol. / Chaudhary, Kaylash; Fehnker, Ansgar; Fehnker, Ansgar; van de Pol, Jan Cornelis; Stoelinga, Mariëlle Ida Antoinette.

Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015). ed. / R.J. van Glabbeek; J.F. Groote; P. Höfner. Australia : Open Publishing Association, 2015. p. 46-60 (Electronic Proceedings in Theoretical Computer Science; Vol. 196).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Modeling and Verification of the Bitcoin Protocol

AU - Chaudhary,Kaylash

AU - Fehnker,Ansgar

AU - Fehnker,Ansgar

AU - van de Pol,Jan Cornelis

AU - Stoelinga,Mariëlle Ida Antoinette

N1 - 10.4204/EPTCS.196.5

PY - 2015/11/13

Y1 - 2015/11/13

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 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)

PB - Open Publishing Association

ER -

Chaudhary K, Fehnker A, Fehnker A, van de Pol JC, Stoelinga MIA. Modeling and Verification of the Bitcoin Protocol. In van Glabbeek RJ, Groote JF, Höfner P, editors, Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015). Australia: Open Publishing Association. 2015. p. 46-60. (Electronic Proceedings in Theoretical Computer Science). Available from, DOI: 10.4204/EPTCS.196.5