Files in this item



application/pdfrdao-analysis.pdf (903kB)
(no description provided)PDF


Title:Statistical Model Checking of RANDAO’s Resilience Against Pre-computed Reveal Strategies
Author(s):Alturki, Musab A.; Rosu, Grigore
formal modeling
statistical model checking
Abstract:Decentralized (pseudo-)random number generation (RNG) is a core process of many emerging distributed systems, including perhaps most prominently, the upcoming Ethereum 2.0 (a.k.a. Serenity) protocol. To ensure security and proper operation, the randomness beacon must be unpredictable and hard to manipulate. A commonly accepted implementation scheme for decentralized RNG is a commit-reveal scheme, known as RANDAO, coupled with a reward system that incentivizes successful participation. However, this approach may still be susceptible to look-ahead attacks, in which an attacker (controlling a certain subset of participants) may attempt to pre-compute the outcomes of (possibly many) reveal strategies, and thus may bias the generated random number to his advantage. To formally evaluate resilience of RANDAO against such attacks, we develop a probabilistic model in rewriting logic of the RANDAO scheme (in the context of Serenity), and then apply statistical model checking and quantitative verification algorithms (using Maude and PVeStA) to analyze two different properties that provide different measures of bias that the attacker could potentially achieve using pre-computed strategies. We show through this analysis that unless the attacker is already controlling a sizable portion of validators and is aggressively attempting to maximize the number of last compromised proposers in the proposers list, the expected achievable bias is quite limited. The full specification of the models developed in this work are available online at
Issue Date:2018-11-19
Genre:Report (Grant or Annual)
Technical Report
Date Available in IDEALS:2018-11-25

This item appears in the following Collection(s)

Item Statistics