Formal Modelling of PBFT Consensus Algorithm in Event-B

The practical Byzantine Fault Tolerance (PBFT) is a classical consensus algorithm that has been widely applied in an alliance blockchain system to make all nodes agree to certain transactions under the assumption that the proportion of Byzantine nodes is no more than 1/3. It is prevalent due to its performance, simplicity, and claimed correctness. However, any vulnerability of the consensus algorithm can lead to a significant loss in finance because no one can change the transaction results after execution. This paper proposes a formal development method of the PBFT algorithm by horizontal refinement in Event-B, which allows us to manage the complexity of the proof process by factoring the proof of correctness into several refinement steps. During the development of PBFT, we have specified the core mechanism like parameterized message types, primary node change, and water-mark interval. Furthermore, we present a mechanical verification of the safety and liveness properties of the model in Rodin, which can be partially and widely used to check the blockchain consensus algorithm vulnerability using a refinement tree of algorithms.