Università degli Studi di Cagliari
reserved
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.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
| main.pdf Solo gestori archivio
Descrizione: Articolo principale
Tipologia: versione pre-print
Dimensione 1 MB
Formato Adobe PDF
|
1 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.