Cryptology ePrint Archive: Report 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 to compiled contracts are also observable in the symbolic model.

Category / Keywords: applications / cryptocurrencies

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

Contact author: bart at unica it

Available format(s): PDF | BibTeX Citation

Note: fixed typo in rule [Action]

Version: 20180510:124624 (All versions of this report)

Short URL:

Discussion forum: Show discussion | Start new discussion

[ Cryptology ePrint archive ]