Cited By
View all- Bartoletti MBracciali ALepore CScalas AZunino R(2021)A Formal Model of Algorand Smart ContractsFinancial Cryptography and Data Security10.1007/978-3-662-64322-8_5(93-114)Online publication date: 1-Mar-2021
Towards a Verified Model of the Algorand Consensus Protocol in Coq
Authors: 
Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña, Grigore RoşuAuthors Info & Claims
Pages 362 - 367
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.
References
[1]
Algorand blockchain features (2019). https://github.com/algorandfoundation/specs/blob/master/overview/Algorand_v1_spec-2.pdf
[2]
Chen, J., Gorbunov, S., Micali, S., Vlachos, G.: ALGORAND AGREEMENT: super fast and partition resilient Byzantine agreement. Cryptology ePrint Archive, Report 2018/377 (2018). https://eprint.iacr.org/2018/377
[3]
Chen J and Micali SAlgorand: a secure and efficient distributed ledgerTheor. Comput. Sci.2019777155-1833961889
[4]
Cohen, C.: Finmap (2019). https://github.com/math-comp/finmap
[5]
Gilad, Y., Hemo, R., Micali, S., Vlachos, G., Zeldovich, N.: Algorand: scaling byzantine agreements for cryptocurrencies. In: SOSP, pp. 51–68 (2017)
[6]
Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008)
[7]
Pîrlea, G., Sergey, I.: Mechanising blockchain consensus. In: CPP, pp. 78–90 (2018)
[8]
Rahli Vincent, Vukotic Ivana, Völp Marcus, and Esteves-Verissimo Paulo Ahmed Amal Velisarios: byzantine fault-tolerant protocols powered by Coq Programming Languages and Systems 2018 Cham Springer 619-650
[9]
Runtime Verification Inc: Algorand verification (2019). https://github.com/runtimeverification/algorand-verification/releases/tag/release-1.1
[10]
Sergey I, Wilcox JR, and Tatlock Z Programming and proving with distributed protocols PACMPL 2018 2 POPL 28:1-28:30
[11]
Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.: Planning for change in a formal verification of the Raft consensus protocol. In: CPP, pp. 154–165 (2016)
Index Terms
- Towards a Verified Model of the Algorand Consensus Protocol in Coq
Index terms have been assigned to the content through auto-classification.
Recommendations
Towards Modeling and Verification of the CKB Block Synchronization Protocol in Coq
Formal Methods and Software EngineeringAbstractThe Nervos CKB (Common Knowledge Base) is the base layer of a new kind of blockchain. The CKB block synchronization protocol provides a set of rules that participating nodes must obey while synchronizing their blocks. This protocol mainly consists ...
Mechanising blockchain consensus
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and ProofsWe present the first formalisation of a blockchain-based distributed consensus protocol with a proof of its consistency mechanised in an interactive proof assistant.
Our development includes a reference mechanisation of the block forest data ...
Making Byzantine consensus live
AbstractPartially synchronous Byzantine consensus protocols typically structure their execution into a sequence of views, each with a designated leader process. The key to guaranteeing liveness in these protocols is to ensure that all correct processes ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Oct 2019
532 pages
ISBN:978-3-030-54993-0
DOI:10.1007/978-3-030-54994-7
© Springer Nature Switzerland AG 2020.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 07 October 2019
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 28 Nov 2024
Other Metrics
Citations
Cited By
View all- Bartoletti MBracciali ALepore CScalas AZunino R(2021)A Formal Model of Algorand Smart ContractsFinancial Cryptography and Data Security10.1007/978-3-662-64322-8_5(93-114)Online publication date: 1-Mar-2021
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in