Verifying liquidity of Bitcoin contracts

Massimo Bartoletti and Roberto Zunino

Abstract

A landmark security property of smart contracts is liquidity: in a non-liquid contract, it may happen that some funds remain frozen. The relevance of this issue is witnessed by a recent liquidity attack to the Ethereum Parity Wallet, which has frozen 160M USD within the contract, making this sum unredeemable by any user. We address the problem of verifying liquidity of Bitcoin contracts. Focussing on itML, a contracts DSL with a computationally sound compiler to Bitcoin, we study various notions of liquidity. Our main result is that liquidity of BitML contracts is decidable, in all the proposed variants. To prove this, we first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of any given set of contracts, abstracting the moves of the context. With respect to the chosen contracts, this abstraction in sound and complete. Our decision procedure for liquidity is then based on model-checking the finite space of states of the abstraction. The computational soundness of the BitML compiler allows to lift this result from the symbolic to the computational level: if our decision procedure establishes that a contract is liquid, then it will be such also under a computational adversary, and vice versa.

Available format(s)
Category
Applications
Publication info
Preprint.
Keywords
Bitcoinsmart contractsverification
Contact author(s)
bart @ unica it
History
2019-02-18: revised
See all versions
Short URL
https://ia.cr/2018/1125

CC BY

BibTeX

@misc{cryptoeprint:2018/1125,
author = {Massimo Bartoletti and Roberto Zunino},
title = {Verifying liquidity of Bitcoin contracts},
howpublished = {Cryptology ePrint Archive, Paper 2018/1125},
year = {2018},
note = {\url{https://eprint.iacr.org/2018/1125}},
url = {https://eprint.iacr.org/2018/1125}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.