Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying Randomized Consensus Protocols with Common Coins

Song Gao, Bohua Zhan, Zhilin Wu, Lijun Zhang

TL;DR

The paper extends probabilistic threshold automata (PTA) to support common coins by introducing a common-coin automaton and communication primitives, enabling verification of randomized fault-tolerant consensus protocols under adaptive Byzantine adversaries. It reformulates multi-round probabilistic correctness into single-round non-probabilistic queries, incorporating a binding-style condition to guard against adaptive attacks. The authors develop an extended counter-system framework, prove reduction theorems, and use ByMC to verify eight common-coin protocols, reproducing known attacks and confirming fixes. The approach broadens parameterized verification capabilities for real-world consensus protocols in cloud and blockchain contexts. Practically, it provides a scalable method to certify correctness properties (agreement, validity, and termination) for complex randomized protocols using common coins.

Abstract

Randomized fault-tolerant consensus protocols with common coins are widely used in cloud computing and blockchain platforms. Due to their fundamental role, it is vital to guarantee their correctness. Threshold automata is a formal model designed for the verification of fault-tolerant consensus protocols. It has recently been extended to probabilistic threshold automata (PTAs) to verify randomized fault-tolerant consensus protocols. Nevertheless, PTA can only model randomized consensus protocols with local coins. In this work, we extend PTA to verify randomized fault-tolerant consensus protocols with common coins. Our main idea is to add a process to simulate the common coin (the so-called common-coin process). Although the addition of the common-coin process destroys the symmetry and poses technical challenges, we show how PTA can be adapted to overcome the challenges. We apply our approach to verify the agreement, validity and almost-sure termination properties of 8 randomized consensus protocols with common coins.

Verifying Randomized Consensus Protocols with Common Coins

TL;DR

The paper extends probabilistic threshold automata (PTA) to support common coins by introducing a common-coin automaton and communication primitives, enabling verification of randomized fault-tolerant consensus protocols under adaptive Byzantine adversaries. It reformulates multi-round probabilistic correctness into single-round non-probabilistic queries, incorporating a binding-style condition to guard against adaptive attacks. The authors develop an extended counter-system framework, prove reduction theorems, and use ByMC to verify eight common-coin protocols, reproducing known attacks and confirming fixes. The approach broadens parameterized verification capabilities for real-world consensus protocols in cloud and blockchain contexts. Practically, it provides a scalable method to certify correctness properties (agreement, validity, and termination) for complex randomized protocols using common coins.

Abstract

Randomized fault-tolerant consensus protocols with common coins are widely used in cloud computing and blockchain platforms. Due to their fundamental role, it is vital to guarantee their correctness. Threshold automata is a formal model designed for the verification of fault-tolerant consensus protocols. It has recently been extended to probabilistic threshold automata (PTAs) to verify randomized fault-tolerant consensus protocols. Nevertheless, PTA can only model randomized consensus protocols with local coins. In this work, we extend PTA to verify randomized fault-tolerant consensus protocols with common coins. Our main idea is to add a process to simulate the common coin (the so-called common-coin process). Although the addition of the common-coin process destroys the symmetry and poses technical challenges, we show how PTA can be adapted to overcome the challenges. We apply our approach to verify the agreement, validity and almost-sure termination properties of 8 randomized consensus protocols with common coins.
Paper Structure (27 sections, 10 theorems, 11 equations, 8 figures, 4 tables)

This paper contains 27 sections, 10 theorems, 11 equations, 8 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Computation Model
  3. Contributions
  4. Outline of the paper
  5. Motivating Protocol and its Attack
  6. The Framework of Probabilistic Threshold Automata Extended with Common Coins
  7. Threshold Automata
  8. Probabilistic Threshold Automata Extended with Common Coins
  9. Environments
  10. Threshold Automata for Correct Processes
  11. Probabilistic Threshold Automata for Common Coins
  12. Extended Probabilistic Counter Systems
  13. Configurations
  14. Actions and Probabilistic Transition Function
  15. Non-probabilistic Extended Counter Systems
  16. ...and 12 more sections

Key Result

Lemma 1

For every Sys$=\mathit{Sys}_\infty$(TA$^n$, TA$^c$) and every $v \in \{0,1\}$, we have: $~\forall k \in \mathbb{N}_0. ~$

Figures (8)

  • Figure 1: Randomized Consensus Protocol MMR14 for Correct Process $\mathcal{P}_i$
  • Figure 2: Naive Voting Protocol for Correct Process $\mathcal{P}_i$
  • Figure 3: Threshold Automaton for Naive Voting
  • Figure 5: The Common Part in the Threshold Automata of (C)
  • Figure 6: A Refined Model of the Common Part
  • ...and 3 more figures

Theorems & Definitions (23)

  • Example 1
  • Example 2
  • Example 3
  • Example 4
  • Definition 1
  • Definition 2: Consensus
  • Lemma 1: Round switch
  • Proof 1
  • Proposition 1
  • Theorem 1
  • ...and 13 more