Towards a verified model of the algorand consensus protocol in coq

Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña, Grigore Roşu

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

Abstract

The Algorand blockchain is a secure and decentralized public ledger based on pure proof of stake rather than proof of work. At its core it is a novel consensus protocol with exactly one block certified in each round: that is, the protocol guarantees that the blockchain does not fork. In this paper, we report on our effort to model and formally verify the Algorand consensus protocol in the Coq proof assistant. Similar to previous consensus protocol verification efforts, we model the protocol as a state transition system and reason over reachable global states. However, in contrast to previous work, our model explicitly incorporates timing issues (e.g., timeouts and network delays) and adversarial actions, reflecting a more realistic environment faced by a public blockchain. Thus far, we have proved asynchronous safety of the protocol: two different blocks cannot be certified in the same round, even when the adversary has complete control of message delivery in the network. We believe that our model is sufficiently general and other relevant properties of the protocol such as liveness can be proved for the same model.

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
PublisherSpringer
Pages362-367
Number of pages6
ISBN (Print)9783030549930
DOIs
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

Conference

Conference3rd World Congress on Formal Methods, FM 2019
CountryPortugal
CityPorto
Period10/7/1910/11/19

Keywords

  • Algorand
  • Blockchain
  • Byzantine consensus
  • Coq

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Towards a verified model of the algorand consensus protocol in coq'. Together they form a unique fingerprint.

  • Cite this

    Alturki, M. A., Chen, J., Luchangco, V., Moore, B., Palmskog, K., Peña, L., & Roşu, G. (2020). Towards a verified model of the algorand consensus protocol in coq. In E. Sekerinski, N. Moreira, J. N. Oliveira, D. Ratiu, R. Guidotti, M. Farrell, M. Luckcuck, D. Marmsoler, J. Campos, T. Astarte, L. Gonnord, A. Cerone, L. Couto, B. Dongol, M. Kutrib, P. Monteiro, & D. Delmas (Eds.), Formal Methods- FM 2019 International Workshops - Revised Selected Papers (pp. 362-367). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12232 LNCS). Springer. https://doi.org/10.1007/978-3-030-54994-7_27