Towards Modeling and Verification of the CKB Block Synchronization Protocol in Coq.

The Nervos CKB (Common Knowledge Base) is the base layer of a new kind of blockchain. The CKB block synchronization protocol provides a set of rules that participating nodes must obey while synchronizing their blocks. This protocol mainly consists of three parts: connecting header, downloading block and accepting block. In this paper, we model the CKB block synchronization protocol in Coq and verify the correctness of the protocol. Our model takes the communication between nodes and the reliability of implementation into consideration to reflect a more realistic environment faced by the blockchain. We prove the soundness and the completeness of the protocol under several reliability and consistency assumptions. We also prove that without some of these assumptions, the protocol may fail to guarantee the correctness of block synchronization. Our formal verification can ensure the security of the protocol and provide ways to prevent potential attacks.