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.

BitML: A Calculus for Bitcoin Smart Contracts / Bartoletti, Massimo; Zunino, Roberto. - (2018), pp. 83-100. (Intervento presentato al convegno ACM CCS tenutosi a Toronto, Canada nel October 15 - 19, 2018) [10.1145/3243734.3243795].

BitML: A Calculus for Bitcoin Smart Contracts

Zunino, Roberto
2018-01-01

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.
2018
Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security
New York, NY
ACM
9781450356930
Bartoletti, Massimo; Zunino, Roberto
BitML: A Calculus for Bitcoin Smart Contracts / Bartoletti, Massimo; Zunino, Roberto. - (2018), pp. 83-100. (Intervento presentato al convegno ACM CCS tenutosi a Toronto, Canada nel October 15 - 19, 2018) [10.1145/3243734.3243795].
File in questo prodotto:
File Dimensione Formato  
main.pdf

Solo gestori archivio

Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 981.8 kB
Formato Adobe PDF
981.8 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/219454
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 49
  • ???jsp.display-item.citation.isi??? 32
social impact