Statistical model checking of randao’s resilience to pre-computed reveal strategies

Musab A. Alturki, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


RANDAO is a commit-reveal scheme for generating pseudo-random numbers in a decentralized fashion. The scheme is used in emerging blockchain systems as it is widely believed to provide randomness that is unpredictable and hard to manipulate by maliciously behaving nodes. However, RANDAO may still be susceptible to look-ahead attacks, in which an attacker (controlling a subset of nodes in the network) may attempt to pre-compute the outcomes of (possibly many) reveal strategies, and thus may bias the generated random number to his advantage. In this work, we formally evaluate resilience of RANDAO against such attacks. We first develop a probabilistic model in rewriting logic of RANDAO, 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 percentage of nodes while aggressively attempting to maximize control of the nodes selected to participate in the process, the expected achievable bias is quite limited.

Original languageEnglish (US)
Title of host publicationFormal Methods- FM 2019 International Workshops - Revised Selected Papers
EditorsEmil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, David Delmas
Number of pages13
ISBN (Print)9783030549930
StatePublished - 2020
Event3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal
Duration: Oct 7 2019Oct 11 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12232 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference3rd World Congress on Formal Methods, FM 2019


  • Blockchain
  • Maude
  • Rewriting logic
  • Statistical model checking

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Statistical model checking of randao’s resilience to pre-computed reveal strategies'. Together they form a unique fingerprint.

Cite this