Conference Proceeding

On Symbolic Verification of Bitcoin's script Language


Klomp R & Bracciali A (2018) On Symbolic Verification of Bitcoin's script Language. In: Garcia-Alfaro J, Herrera-Joancomartí J, Livraga G & Rios R (eds.) Data Privacy Management, Cryptocurrencies and Blockchain Technology. DPM 2018, CBT 2018. Lecture Notes in Computer Science, 11025. Data Privacy Management, Cryptocurrencies and Blockchain Technology 2018, Barcelona, Spain, 06.09.2018-07.09.2018. Cham, Switzerland: Springer International Publishing, pp. 38-56.

Validation of Bitcoin transactions rely upon the successful execution of scripts written in a simple and effective, non-Turing-complete by design language, simply called SCRIPT. This makes the validation of closed scripts, i.e. those associated to actual transactions and bearing full information, straightforward. Here we address the problem of validating open scripts, i.e. we address the validation of redeeming scripts against the whole set of possible inputs, i.e. under which general conditions can Bitcoins be redeemed? Even if likely not one of the most complex languages and demanding verification problems, we advocate the merit of formal verification for the Bitcoin validation framework. We propose a symbolic verification theory for of open SCRIPT, a verifier tool-kit, and illustrate examples of use on Bitcoin transactions. Contributions include 1) a formalisation of (a fragment of) the language; 2) a novel symbolic approach to SCRIPT verification, suitable, e.g. for the verification of newly defined and non-standard payment schemas; and 3) building blocks for a larger verification theory for the developing area of Bitcoin smart contracts. The verification of smart contracts, i.e. agreements built as transaction-based protocols, is currently a difficult to formalise and computationally demanding problem.

Title of seriesLecture Notes in Computer Science
Number in series11025
Publication date31/12/2018
Publication date online07/09/2018
PublisherSpringer International Publishing
Place of publicationCham, Switzerland
ISSN of series0302-9743
ISBN9783030003043; 9783030003050
ConferenceData Privacy Management, Cryptocurrencies and Blockchain Technology 2018
Conference locationBarcelona, Spain