The Consensus Machine: Formalising Consensus in the Presence of Malign Agents (Preliminary)
A.W. Roscoe, Pedro Antonino, Jonathan Lawrence
University College Oxford Blockchain Research Centre, The Blockhouse Technology Ltd
We show how a group of independent agents with carefully specified notions of progress and synchronisation can proceed in a model where consensus does not require unanimity and represents an emergent group behaviour. These agents will typically cooperate to implement a decentralised system such as a blockchain. Thus a model state machine can be compiled into replicated asynchronous agents that implement it in such a way as to overcome Byzantine faults up to a certain assumed level. Our abstraction achieves precise reliability and allows us to create schemes in which multiple consensus machines interact that can be modelled in process algebras like CSP and verified by model checking. This paper concentrates on the CSP analysis of a protocol showing how one distributed consensus machine can take over control from another without creating ambiguity over the outcome.