A stochastic analysis of the Gasper protocol

Abstract

Ethereum has recently switched to a Proof of Stake consensus protocol called Gasper. We analyze Gasper using PRISM+ , an extension of the probabilistic model checker PRISM with primitives for modeling blockchain data types . PRISM+ is therefore used to rapidly and automatically analyze the robustness of Gasper when tuning, up or down, several basic parameters of the protocol, such as network latencies and number of validators. We also study the effectiveness of Gasper in updating stakes and its resilience to three attacks: the balance, bouncing and time attacks.