Modeling and Verifying the CKB Blockchain Consensus Protocol

Meng Sun, Yuteng Lu, Yichun Feng, Qi Zhang and Shaoying Liu
Additional contact information
Meng Sun: School of Mathematical Sciences, Peking University, Beijing 100871, China
Yuteng Lu: School of Mathematical Sciences, Peking University, Beijing 100871, China
Yichun Feng: School of Mathematical Sciences, Peking University, Beijing 100871, China
Qi Zhang: School of Mathematical Sciences, Peking University, Beijing 100871, China
Shaoying Liu: Graduate School of Advanced Science and Engineering, Hiroshima University, Higashi Hiroshima City 739-8527, Japan

Mathematics, 2021, vol. 9, issue 22, 1-15

Abstract: The Nervos CKB (Common Knowledge Base) is a public permissionless blockchain designed for the Nervos ecosystem. The CKB consensus protocol is the key protocol of the Nervos CKB, which improves the limit of the consensus’s performance for Bitcoin. In this paper, we developed the formal model of the CKB consensus protocol using timed automata. Based on the model, we formally verified various important properties of the Nervos CKB to provide a sufficient trustworthiness assurance. Especially, the security of the Nervos CKB against the selfish mining attacks to the protocol was investigated.

Keywords: Nervos CKB; consensus protocol; model checking; UPPAAL (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2021
References: View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
https://www.mdpi.com/2227-7390/9/22/2954/pdf (application/pdf)
https://www.mdpi.com/2227-7390/9/22/2954/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:9:y:2021:i:22:p:2954-:d:682761

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().