Modelling schemes for multi-party blockchain-based systems to support integrity analysis

Multi-party systems are important for business processes but can be complex. Blockchain facilitates trust in multiparty systems by providing transparency, decentralised control, and immutable transaction history, to improve security and accountability between parties. The use of cryptographic hashes and the continual validation of the shared ledger in a blockchain system provides parties with data integrity for historical transactions and process integrity for smart contract execution. However, in the design of a broader system combining a blockchain with off-chain components, it is not always clear how system-level integrity is supported. This paper proposes two modelling schemes to better understand blockchain's support for integrity in multi-party blockchain-based systems. The schemes model interactions between components in an architecture as security protocols, for analysis by standard techniques and tools. We first illustrate how blockchain-based systems can be abstractly modelled directly as security protocols. Then we show how blockchain-specific issues such as consensus-based 'forking' (also known as 'orphan blocks' or 'uncle blocks') can be encoded. This allows transaction reordering behaviour to manifest in the model, and allows design mitigation for that problem to be checked. We illustrate our approach with analyses of three design alternatives for possible enhancements to a multi-party system for sharing trade certificates.