Paper 2018/122
BitML: a calculus for Bitcoin smart contracts
Massimo Bartoletti and Roberto Zunino
Abstract
We propose a domain-specific language for smart contracts, which allows participants to transfer cryptocurrency according to agreed contract terms. We define a symbolic and a computational model for reasoning about their security. In the symbolic model, participants act according to the semantics of the domain-specific language. Instead, in the computational model they exchange bitstrings, and publish transactions on the Bitcoin blockchain. A compiler is provided to translate smart contracts into standard Bitcoin transactions. We prove the correctness of our compiler, showing that computational attacks to compiled smart contracts are also observable in the symbolic model.
Note: fixed typo in rule [Action]
Metadata
- Available format(s)
- Category
- Applications
- Publication info
- Preprint. MINOR revision.
- 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
-
CC BY