Verifying Randomized Byzantine Agreement

摘要

Distributed systems increasingly rely on fault-tolerant and secure authorization services. An essential primitive used to implement such services is the Byzantine agreement protocol for achieving agreement among n parties even if t parties (t < n/3) are corrupt and behave maliciously. We describe our experience verifying the randomized protocol ABBA (Asynchronous Binary Byzantine Agreement) of Cachin, Kursawe and Shoup, a practical protocol that incorporates modern threshold-cryptographic techniques and forms a core of powerful asynchronous broadcast protocols. The protocol is efficient (runs in constant expected time), optimal (it tolerates the maximum number of corrupted parties) and provably secure (in the random oracle model). We model the protocol in Cadence SMV, replacing the coin tosses with nondeterministic choice, and provide a proof of the protocol correctness for all n under the assumption that the cryptographic primitives are correct. The proof is fully automated except for one high-level inductive argument involving probabilistic reasoning. We validate probabilistic reasoning through deriving abstractions for finite configurations (for n up to 20) and model checking those with the probabilistic model checker PRISM.