BitML: A calculus for bitcoin smart contracts

Massimo Bartoletti;
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
Inglese
Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security
9781450356930
ACM
83
100
18
WOS:000461315900007
2-s2.0-85056446553
25th ACM Conference on Computer and Communications Security, CCS 2018
Contributo
Comitato scientifico
October 15-19, 2018
Toronto, Canada
internazionale
scientifica
no
4 Contributo in Atti di Convegno (Proceeding)::4.1 Contributo in Atti di convegno
Bartoletti, Massimo; Zunino, Roberto
273
2
4.1 Contributo in Atti di convegno
reserved
info:eu-repo/semantics/conferencePaper
Files in This Item:
File Size Format  
main.pdf

Solo gestori archivio

Description: Articolo principale
Type: versione pre-print
Size 1 MB
Format Adobe PDF
& nbsp; View / Open   Request a copy
1 MB Adobe PDF & nbsp; View / Open   Request a copy

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Questionnaire and social

Share on:
Impostazioni cookie