Paper 2018/122

BitML: A Calculus for Bitcoin Smart Contracts

Massimo Bartoletti and Roberto Zunino

Abstract

We introduce BitML, a domain-specific language for specifying contracts that regulate transfers of bitcoins among participants, without relying on trusted intermediaries. We define a symbolic and a computational model for reasoning about BitML security. In the symbolic model, participants act according to the semantics of BitML, while in the computational model they exchange bitstrings, and read/append transactions on the Bitcoin blockchain. A compiler is provided to translate contracts into standard Bitcoin transactions. Participants can execute a contract by appending these transactions on the Bitcoin blockchain, according to their strategies. We prove the correctness of our compiler, showing that computational attacks on compiled contracts are also observable in the symbolic model.

Note: Added remark on replay attacks

Metadata
Available format(s)
PDF
Category
Applications
Publication info
Published elsewhere. Major revision. ACM CCS 2018
Keywords
cryptocurrencies
Contact author(s)
bart @ unica it
History
2018-10-03: last of 5 revisions
2018-02-01: received
See all versions
Short URL
https://ia.cr/2018/122
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2018/122,
      author = {Massimo Bartoletti and Roberto Zunino},
      title = {BitML: A Calculus for Bitcoin Smart Contracts},
      howpublished = {Cryptology ePrint Archive, Paper 2018/122},
      year = {2018},
      note = {\url{https://eprint.iacr.org/2018/122}},
      url = {https://eprint.iacr.org/2018/122}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.