A Formal Model of Algorand BBA∗ Consensus with Its Noninterference Analysis and Probabilistic Verification via CADP

Algorand is a scalable and secure permissionless blockchain that achieves proof-of-stake-based consensus via binary Byzantine agreement and cryptographic self-sortition. In this paper we present a process algebraic model of the Algorand consensus protocol, which captures the behavior of participants in terms of the alternation of steps toward a committee-based agreement. We use the model to study the robustness of the protocol with respect to malicious participants, which may try to boy- cott the commitment of the proposed block, as well as the probabilities of committing the proposed block or an empty one after a boycott attempt. Our process algebraic model is translated into LNT, the language of the CADP toolset, to investigate robustness via a novel application of equivalence-checking-based noninterference analysis, which we have implemented in CADP through its script verification language SVL.