Paper 2019/415

Refinement and Verification of CBC Casper

Ryuya Nakamura, Takayuki Jimba, and Dominik Harz

Abstract

Decentralised ledgers are a prime application case for consensus protocols. Changing sets of validators have to agree on a set of transactions in an asynchronous network and in the presence of Byzantine behaviour. Major research efforts focus on creating consensus protocols under such conditions, with proof-of-stake (PoS) representing a promising candidate. PoS aims to reduce the waste of energy inherent to proof-of-work (PoW) consensus protocols. However, a significant challenge is to get PoS protocols "right", i.e. ensure that they are secure w.r.t. safety and liveness. The "Correct-by-Construction" (CBC) Casper approach by the Ethereum project employs pen-and-paper proofs to ensure its security. CBC Casper is a framework to define consensus protocols and aims to prove safety without loss of abstractness. Each member of the CBC Casper family of protocols is defined by five parameters. CBC Casper models the protocol by a state of each validator and messages sent by validators. Each validator can transition its state using messages by other validators that include their current consensus value and a justification (i.e. their previous messages). We extend CBC Casper in three ways. First, we summarise the research of CBC Casper and extend the definitions of safety and liveness properties. To this end, we discuss an instance of CBC Casper called Casper The Friendly GHOST (TFG), a consensus protocol using a variant of the GHOST fork-choice rule. Second, we refine the properties of messages and states in CBC Casper and give a definition of blockchain safety for Casper TFG. Third, we formally verify the CBC Casper framework together with our refined message and state properties as well as our blockchain safety definition in the Isabelle/HOL proof assistant.

Note: Isabelle proofs are available at https://github.com/LayerXcom/cbc-casper-proof

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Minor revision.2019 Crypto Valley Conference on Blockchain Technology (CVCBT)
Keywords
blockchainconsensus protocolproof-of-stakeEthereumformal verificationIsabelle
Contact author(s)
nrryuya @ gmail com
takayuki jinba @ layerx co jp
d harz @ imperial ac uk
History
2019-12-17: last of 5 revisions
2019-04-24: received
See all versions
Short URL
https://ia.cr/2019/415
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2019/415,
      author = {Ryuya Nakamura and Takayuki Jimba and Dominik Harz},
      title = {Refinement and Verification of CBC Casper},
      howpublished = {Cryptology ePrint Archive, Paper 2019/415},
      year = {2019},
      note = {\url{https://eprint.iacr.org/2019/415}},
      url = {https://eprint.iacr.org/2019/415}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.