Hybrid Casper is the new Ethereum blockchain protocol that uses both Proof of Work and Proof of Stake to reach a consensus between nodes. Here, we analyse the protocol using PRISM+, an extension of the probabilistic model checker PRISM with primitives for expressing blockchain data types. First, we extend PRISM+ to include data types and operations for modelling and analysing Proof of Stake-based consensus protocols. Then, we model Hybrid Casper in PRISM+ as a parallel composition of stochastic processes, thus precisely describing the behaviour of the protocol and highlighting its corner cases. PRISM+ is therefore used to rapidly and automatically analyse the resilience of Hybrid Casper when tuning, up or down, several basic parameters of the protocol, such as the rates of creating blocks, and the strategies for determining penalties. Finally, we study the robustness of Hybrid Casper to two well known attacks: the Eclipse attack and the majority attack.

Resilience of Hybrid Casper under varying values of parameters

Galletta, Letterio
;
Mercanti, Ivan;
2022-01-01

Abstract

Hybrid Casper is the new Ethereum blockchain protocol that uses both Proof of Work and Proof of Stake to reach a consensus between nodes. Here, we analyse the protocol using PRISM+, an extension of the probabilistic model checker PRISM with primitives for expressing blockchain data types. First, we extend PRISM+ to include data types and operations for modelling and analysing Proof of Stake-based consensus protocols. Then, we model Hybrid Casper in PRISM+ as a parallel composition of stochastic processes, thus precisely describing the behaviour of the protocol and highlighting its corner cases. PRISM+ is therefore used to rapidly and automatically analyse the resilience of Hybrid Casper when tuning, up or down, several basic parameters of the protocol, such as the rates of creating blocks, and the strategies for determining penalties. Finally, we study the robustness of Hybrid Casper to two well known attacks: the Eclipse attack and the majority attack.
File in questo prodotto:
File Dimensione Formato  
preprintpos.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: Nessuna licenza
Dimensione 782.05 kB
Formato Adobe PDF
782.05 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
s11238-021-09841-0 (1).pdf

accesso aperto

Tipologia: Versione Editoriale (PDF)
Licenza: Creative commons
Dimensione 1.78 MB
Formato Adobe PDF
1.78 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11771/22218
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
social impact