Models for Bitcoin smart contracts

Venue: Department of Mathematics, via Sommarive, 14 - Povo (TN) - Seminar Room "-1"
At: 4.00 pm

Speaker:

• Massimo Bartoletti (University of Cagliari)

Abstract:

Albeit the primary usage of Bitcoin is to exchange currency, its blockchain and consensus mechanism can also be exploited to securely execute some forms of smart contracts. These are agreements among mutually distrusting parties, which can be automatically enforced without resorting to a trusted intermediary. However, the existing informal, low-level descriptions, and the use of poorly documented Bitcoin features, pose obstacles to the research in this field. We present a formal model of Bitcoin transactions, which is sufficiently abstract to enable formal reasoning, for instance proving well-formedness properties of the Bitcoin blockchain like the absence of double-spending. We then show how to use our model as a concrete layer upon which designing higher-level specification languages for smart contracts.

Contact person: Massimiliano Sala