Cryptology ePrint Archive: Report 2019/415

Refinement and Verification of CBC Casper

Ryuya Nakamura and 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 for decentralised ledgers. 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. Security proofs are provided using pen-and-paper approaches including the "Correct-by-Construction" (CBC) Casper proposed by the Ethereum project. CBC Casper's design philosophy deviates from traditional consensus protocols as it is an abstract framework to define consensus protocols and aims to prove its correctness 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 CBC Casper together with our additional properties in the Isabelle/HOL proof assistant.

Category / Keywords: cryptographic protocols / blockchain, consensus protocol, proof-of-stake, Ethereum, formal verification, Isabelle

Date: received 18 Apr 2019, last revised 3 May 2019

Contact author: nrryuya at gmail com,takayuki jinba@layerx co jp,d harz@imperial ac uk

Available format(s): PDF | BibTeX Citation

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

Version: 20190504:011416 (All versions of this report)

Short URL: ia.cr/2019/415


[ Cryptology ePrint archive ]