Refinement and Verification of CBC Casper

Ryuya Nakamura; Takayuki Jimba; Dominik Harz

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: blockchain consensus protocol proof-of-stake Ethereum formal verification Isabelle
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: 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},
      url = {https://eprint.iacr.org/2019/415}
}