Renegotiation and recursion in Bitcoin contracts
This work addresses the problem of inflexibility in Bitcoin smart contracts for developers and users, allowing more complex financial contracts, though it is incremental as it builds upon existing BitML.
The paper tackles the limitation of BitML, a smart contract calculus for Bitcoin, by introducing a new primitive for contract renegotiation, enabling participants to modify terms at run-time and express recursive contracts, while maintaining execution on standard Bitcoin with preserved security guarantees.
BitML is a process calculus to express smart contracts that can be run on Bitcoin. One of its current limitations is that, once a contract has been stipulated, the participants cannot renegotiate its terms: this prevents expressing common financial contracts, where funds have to be added by participants at run-time. In this paper, we extend BitML with a new primitive for contract renegotiation. At the same time, the new primitive can be used to write recursive contracts, which was not possible in the original BitML. We show that, despite the increased expressiveness, it is still possible to execute BitML on standard Bitcoin, preserving the security guarantees of BitML.