Modelling and analysing a simple blockchain using CSP and FDR
A.W. Roscoe, Jonathan Lawrence
University College Oxford Blockchain Research Centre, The Blockhouse Technology Ltd
We present a CSP (Communicating Sequential Processes) model of a simple blockchain system and its analysis using the refinement checking tool FDR (Failures Divergences Refinement). We build on ideas developed for the successful models of cryptographic protocols that model adversary behaviours symbolically, and introduce new ways of recording and communicating large and implic- itly recursive data values, namely blocks that include hashes of other blocks. We propose a model for malign agents that is similar to the intruder model for protocols. We illustrate how blockchains work and how bad decisions can lead to pathologies such as forking, diagnosed by tracking the evo- lution of the blockchain. We discuss potential ways of using CSP and FDR to model other aspects of blockchains and decentralised systems.