Formal Modeling and Verification of the Algorand Consensus Protocol in CADP

TL;DR

This paper presents a formal process algebraic model of the Algorand blockchain consensus protocol to verify its correctness and analyze its robustness against malicious attacks using the CADP toolkit.

Contribution

It introduces a novel formal model of Algorand's consensus process and evaluates its security properties under adversarial conditions.

Findings

Protocol is correct without adversaries

Malicious nodes can force empty block commits

Formal methods reveal protocol robustness and limitations

Abstract

Algorand is a scalable and secure permissionless blockchain that achieves proof-of-stake consensus via cryptographic self-sortition and binary Byzantine agreement. 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 validate the correctness of the protocol in the absence of adversaries and then extend our model to assess the influence of coordinated malicious nodes that can force the commit of an empty block instead of the proposed one. The adversarial scenario is analyzed through an equivalence-checking-based noninterference framework that we have implemented in the CADP verification toolkit. In addition to highlighting both the robustness and the limitations of the Algorand protocol under adversarial assumptions, this work illustrates the added value of using formal methods for the analysis of consensus algorithms within blockchains.