Validation of decentralised smart contracts through game theory and formal methods

Giancarlo Bigi, Andrea Bracciali, Giovanni Meacci and Emilio Tuosto


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

My Home Page