Cryptology ePrint Archive: Report 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.

Category / Keywords: applications / cryptocurrencies

Date: received 31 Jan 2018, last revised 10 Feb 2018

Contact author: bart at unica it

Available format(s): PDF | BibTeX Citation

Note: fixed typo in rule [Action]

Version: 20180210:102532 (All versions of this report)

Short URL:

Discussion forum: Show discussion | Start new discussion

[ Cryptology ePrint archive ]