Validation of decentralised smart contracts through game theory and formal methods
Giancarlo Bigi, Andrea Bracciali, Giovanni Meacci and Emilio Tuosto
Summary
The introduction of the BitCoin protocol in 2008 has strongly pushed forward
the development of decentralised distributed systems. BitCoin is decentralised
since it is not controlled by any central coercing authority. Rather, a computationally
expensive distributed consensus over the internet certifies its transitions,
for instance preventing the double expenditure of immaterial money. Due to the
computational costs involved, the consensus of the whole BitCoin network over
the internet cannot realistically be overturned. Although BitCoin has been
highly volatile and associated to illegal activities, institutional players, including
governments and banks, as well as the general public, have shown interest in it.
BitCoin has started to appear as a potentially reliable and enabling technology.
Currently, the next step builds on top of BitCoin, aiming to introduce decentralised
distributed technologies on a larger scale. One example of this are decentralised
smart contracts, i.e. protocols designed to define self-enforcing contracts
amongst untrusted and independent players. BitHalo is a paradigmatic, very
recent and innovative example of a decentralised smart contract.
The validation of such protocols is clearly highly desirable and, as usual,
very complex. Interestingly, the distributed and decentralised aspects of smart
contracts add to complexity since free choices and gaming strategies come into
play. Protocols are run by autonomous players, possibly mixing physical actions,
e.g. the shipment of goods, and computer-mediated ones, e.g. an electronic payment,
without any possibility of a coercing central authority. Differently from
more traditional protocols, a sort of socio-economical aspect becomes relevant
for the validation of smart contracts.
In this paper, we analyse and validate DSCP, an idealised smart contract
inspired by BitHalo. A distinguished feature of our approach is the combination
of game theory and formal methods to suitably address the mentioned
complexity of the analysis and validation of smart contracts. Game theory has
been widely exploited to analyse how contracts are settled through bargaining
procedures but the analysis of protocols that enforce
contracts is a novel area of application. Formal methods have been extensively
used for protocol validation, from security protocols to the more recent behavioural
contracts of application level protocols. However, it is worth remarking
that such kind of contracts and the contracts supported by BitHalo exist in
different contexts and for different purposes. Indeed, in behavioural contracts
the main focus is to ensure that the parallel composition of distributed participants
does not yield communication problems such as deadlocks or to analyse communication misbehaviours in untrusted settings.
Noticeably, BitHalo also embeds steps that depend
upon decisions made by human players, which do not appear in application level
protocols.
In our framework game theory and formal methods complement each other:
the former caters for the study of the gaming strategy aspects, while the latter
provide the grounds for a precise definition of the protocol and related working
hypotheses. Furthermore, the probabilistic framework we adopted allows us to
properly model uncertainty and non-determinism in players' behaviour, and to
exploit effective automated techniques, like statistical model checking, to validate
the properties of the smart contract. To the best of our knowledge, the proposed
combined approach is here firstly applied to the validation of smart contracts.
A detailed analysis of DSCP is carried out both analytically from the viewpoint
of game theory, and computationally, via the definition of a model, the
properties of interest, and their validation through probabilistic model checking.
Sensitivity of various parameters is studied, including monetary values and
fraudulence profiles of the players. Our combined analysis formally and quantitatively
clarifies the intended behaviour of the protocol, which relies on a
deposit scheme to enforce trust. Sometimes, assumptions on the deposit scheme
may result in being unrealistic. Our analysis explores the details of the system
under the uncertainty introduced when the deposit enforcing trust assumption is
weakened.
The original paper is available at http://dx.doi.org/10.1007/978-3-319-25527-9_11.
My Home Page