Modeling and Verification of Algorand BBA* Consensus

Algorand is a scalable and secure permissionless blockchain that achieves proof-of-stake-based consensus via binary Byzantine agreement BBA∗and cryptographic self-sortition. In this paper we present a process algebraic model of the Algorand consensus protocol with the aim of enabling formal verification. Our model captures the behavior of participants in terms of the structured alternation of consensus steps toward a committee-based agreement. We verify the robustness of the protocol in the presence of coordinated malicious participants that may try to force the commitment of an empty block instead of the proposed one. The verification of our pure process algebraic model translated in the LNT language is conducted through a novel application of equivalence- checking-based noninterference analysis, which we have implemented in the CADP toolkit through its script verification language SVL.