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.
Laneve, C., Veschetti, A. (2025). A stochastic analysis of the Gasper protocol. COMPUTER COMMUNICATIONS, 236, 1-13 [10.1016/j.comcom.2025.108123].
A stochastic analysis of the Gasper protocol
Laneve C.;
2025
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
