@inproceedings{1428f2c1706649189c4f8d6bf6f795f9,
title = "Statistical model checking of randao{\textquoteright}s resilience to pre-computed reveal strategies",
abstract = "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.",
keywords = "Blockchain, Maude, RANDAO, Rewriting logic, Statistical model checking",
author = "Alturki, {Musab A.} and Grigore Ro{\c s}u",
note = "Funding Information: Acknowledgements. We thank Danny Ryan and Justin Drake from the Ethereum Foundation for their very helpful comments. This work was performed under the first Ethereum Foundation security grant “Casper formal verification” [10]. Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2020.; 3rd World Congress on Formal Methods, FM 2019 ; Conference date: 07-10-2019 Through 11-10-2019",
year = "2020",
doi = "10.1007/978-3-030-54994-7_25",
language = "English (US)",
isbn = "9783030549930",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "337--349",
editor = "Emil Sekerinski and Nelma Moreira and Oliveira, {Jos{\'e} N.} and Daniel Ratiu and Riccardo Guidotti and Marie Farrell and Matt Luckcuck and Diego Marmsoler and Jos{\'e} Campos and Troy Astarte and Laure Gonnord and Antonio Cerone and Luis Couto and Brijesh Dongol and Martin Kutrib and Pedro Monteiro and David Delmas",
booktitle = "Formal Methods- FM 2019 International Workshops - Revised Selected Papers",
address = "Germany",
}