Modeling Bitcoin contracts by timed automata

DOI10.1007/978-3-319-10512-3_2zbMATH Open1448.91328arXiv1405.1861OpenAlexW4993390WikidataQ111687910 ScholiaQ111687910MaRDI QIDQ5500550FDOQ5500550

Łukasz Mazurek, Daniel Malinowski, Marcin Andrychowicz, Stefan Dziembowski

Publication date: 6 August 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: Bitcoin is a peer-to-peer cryptographic currency system. Since its introduction in 2008, Bitcoin has gained noticeable popularity, mostly due to its following properties: (1) the transaction fees are very low, and (2) it is not controlled by any central authority, which in particular means that nobody can "print" the money to generate inflation. Moreover, the transaction syntax allows to create the so-called contracts, where a number of mutually-distrusting parties engage in a protocol to jointly perform some financial task, and the fairness of this process is guaranteed by the properties of Bitcoin. Although the Bitcoin contracts have several potential applications in the digital economy, so far they have not been widely used in real life. This is partly due to the fact that they are cumbersome to create and analyze, and hence risky to use. In this paper we propose to remedy this problem by using the methods originally developed for the computer-aided analysis for hardware and software systems, in particular those based on the timed automata. More concretely, we propose a framework for modeling the Bitcoin contracts using the timed automata in the UPPAAL model checker. Our method is general and can be used to model several contracts. As a proof-of-concept we use this framework to model some of the Bitcoin contracts from our recent previous work. We then automatically verify their security in UPPAAL, finding (and correcting) some subtle errors that were difficult to spot by the manual analysis. We hope that our work can draw the attention of the researchers working on formal modeling to the problem of the Bitcoin contract verification, and spark off more research on this topic.

Full work available at URL: https://arxiv.org/abs/1405.1861

Recommendations

• Formal verification of fair exchange based on Bitcoin smart contracts
• Cryptocash, cryptocurrencies, and cryptocontracts
• Bitcoin private key locked transactions
• How to use bitcoin to design fair protocols
• The Bitcoin Backbone Protocol: Analysis and Applications

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Actuarial science and mathematical finance (91G99)

Cited In (27)

• Modeling and analysis of block arrival times in the Bitcoin blockchain
• Title not available (Why is that?)
• Bicorn: an optimistically efficient distributed randomness beacon
• Eagle: efficient privacy preserving smart contracts
• McFly: verifiable encryption to the future made practical
• Blind polynomial evaluation and data trading
• P2DEX: privacy-preserving decentralized cryptocurrency exchange
• (Public) verifiability for composable protocols without adaptivity or zero-knowledge
• Incentive-driven attacker for corrupting two-party protocols
• Game theoretic notions of fairness in multi-party coin toss
• Coin-based multi-party fair exchange
• How to build time-lock encryption
• Financially backed covert security
• FAST: fair auctions via secret transactions
• A formal model of Algorand smart contracts
• Shielded computations in smart contracts overcoming forks
• Designing Proof of Human-Work Puzzles for Cryptocurrency and Beyond
• Cryptographic algorithms for privacy-preserving online applications
• Absentia: secure multiparty computation on ethereum
• Abuse resistant law enforcement access systems
• TARDIS: a foundation of time-lock puzzles in UC
• Game-Theoretic Analysis of an Incentivized Verifiable Computation System
• Accountable Storage
• Fully-secure MPC with minimal trust
• Expected linear round synchronization: the missing link for linear Byzantine SMR
• \(\log^\ast\)-round game-theoretically-fair leader election
• Bankrupting Sybil despite churn

Uses Software

• Kronos
• TIMES
• Uppaal

This page was built for publication: Modeling Bitcoin contracts by timed automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5500550)