“Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods”, 2015-11-20 (; similar):
Decentralised smart contracts represent the next step in the development of protocols that support the interaction of independent players without the presence of a coercing authority. Based on protocols à la BitCoin for digital currencies, smart contracts are believed to be a potentially enabling technology for a wealth of future applications.
The validation of such an early developing technology is as necessary as it is complex. In this paper we combine game theory and formal models to tackle the new challenges posed by the validation of such systems [as BitHalo].
…The purpose of BitHalo is to create unbreakable trade contracts without the need of arbiters or escrow agents, lowering substantially the costs for the 2 parties involved in the contract. Since it does not require trust, nothing in the BitHalo system is centralised. It does not require a server, just the Internet. Its peer-to-peer communication system allows the 2 parties to use email, Bitmessage, IRC, or other methods to exchange messages and data. BitHalo is off-blockchain in the sense that the record of BitHalo contracts is not kept in the blockchain, and therefore the use of BitHalo will not bloat the blockchain.
BitHalo can be used for bartering, self-insuring, backing commodities, performing derivatives, making good-faith employment contracts, performing 2-party escrow, and more general business contracts.
Transactions are insured by a deposit in one of the supported digital currencies (including BTC) on a joint account, double-deposit escrow. The BitHalo protocol forces each party to uphold the contract in order to achieve the most economically optimal outcome. In a typical contract exchanging a payment for goods or services, the payment can be sent either separately, using checks, money transfer, crypto-currencies, etc., or paid directly with the deposit. The deposit will only be refunded to both parties on shared consent, which has to be expressed by both parties. In the lack of expression of shared consent, the joint account will self-destruct after a time-out. Time limits and deposit amounts are all flexible and agreed upon by both parties. Dissatisfaction about the outcome of the transaction by one of the parties, for instance because of theft or deception, will lead to the destruction of the deposit due to the lack of shared consensus. When the deposit exceeds the amount being transacted, the loss typically results larger than the benefits possibly obtainable by a fraudulent behavior. However, deposits exceeding the transacted amount may be in some cases unfeasible. In some situations, smaller deposits may incentivize one or both parties to break the contract.
…As standard, DSCP allows 2 parties, ie. the 2 players of the protocol, to autonomously exchange money against goods without the need of a centralised arbiter. It is worth remarking that the 2 players are completely independent, not subject to any third party authority in the execution of the exchange protocol, and can, for instance, decide to leave the protocol at any time…DSCP is based on the mentioned notion of “enforced trust” in the fact that none of the 2 parties will ever be in a position in which breaking the protocol is for them advantageous. We will see that this, as expected, will be properly enforced only when the deposit, whose payment is a pre-requisite for the execution of the protocol, exceeds the value of the goods.