# Generalized Paxos Made Byzantine
## 5 Byzantine Fault Tolerant Protocol
### Agreement Protocol
Please note that since the acceptors also leave the checkpointing command in their sequence of proven commands, every valid subsequent sequence will begin with \(C^{*}\). The purpose of this command is to allow a learner to detect when an incoming message was reordered. The learner can check the first position of an incoming sequence against the first position of its _learned_ and, if a mismatch is detected, it knows that either a pre and post-checkpoint message has been reordered. When performing this check, two possible anomalies that can occur: either (1) the first position of the incoming sequence contains a \(C^{*}\) command and the learner's _learned_ sequence does not, in which case the incoming sequence was sent post-checkpoint and the learner is missing a sequence containing the respective checkpoint command; or (2) the first position of the _learned_ sequence contains a checkpoint command and the incoming sequence does not, in which case the incoming sequence was assembled pre-checkpoint and the learner has already executed the checkpoint. In the first case, the learner can simply store the post-checkpoint sequences until it receives the sequence containing the appropriate \(C^{*}\) command at which point it can learn the stored sequences. Please note that the order in which the post-checkpoint sequences are executed is irrelevant since they're extensions of each other. In the second case, the learner receives sequences sent before the checkpoint sequence that it has already executed. In this scenario, the learner can simply discard these sequences since it knows that it executed a subsequent sequence (i.e., the one containing the checkpoint command) and proven sequences are guaranteed to be extensions of previous proven sequences. To simplify the algorithm presentation, this extension to the protocol is not included in the pseudocode description. ## 6 Correctness Proofs

This section argues for the correctness of the Byzantine Generalized Paxos protocol in terms of the specified consensus properties (Table 1 summarizes the BGP proof notation). ### Consistency

**Theorem 1**. : _At any time and for any two correct learners \(l_{i}\) and \(l_{j}\), \(learned_{l_{i}}\) and \(learned_{l_{j}}\) can subsequently be extended to equivalent sequences._

Proof. :
1. At any given instant, \(\forall s,s^{\prime}\in\mathcal{P},\forall l_{i},l_{j}\in\mathcal{L},learned( l_{j},s)\wedgelearned(l_{i},s^{\prime})\implies\exists\sigma_{1},\sigma_{2}\in \mathcal{P}\cup\{\bot\},s\,\bullet\sigma_{1}\sim s^{\prime}\bullet\sigma_{2}\)

Proof. :

\begin{table}
\begin{tabular}{c c} \hline \hline
**Invariant/Symbol** & **Definition** \\ \hline \(\sim\) & Equivalence relation between sequences \\ \(X\,\



At any given instant, \(\forall s,s^{\prime}\in\mathcal{P},\forall l_{i},l_{j}\in\mathcal{L},learned(l_{i},s )\wedgelearned(l_{j},s^{\prime})\implies(maj\_accepted(s,b)\vee(min\_ accepted(s,b)\wedge s\bullet\sigma_{1}\sim x\bullet\sigma_{2}))\wedge(maj\_accepted(s^{\prime},b^{ \prime})\vee(min\_accepted(s^{\prime},b^{\prime})\wedge s^{\prime}\bullet \sigma_{1}\sim x\bullet\sigma_{2}))\), \(\exists\sigma_{1},\sigma_{2}\in\mathcal{P}\cup\{\bot\},\forall x\in\mathcal{P},\forall b,b^{\prime}\in\mathcal{B}\)

**Proof:** A sequence can only be learned in some ball \(b\) if the learner gathers \(N-f\) votes (i.e., \(maj\_accepted(s,b)\)), each containing \(N-f\) valid proofs, or if it is universally commutative (i.e., \(s\bullet\sigma_{1}\sim x\bullet\sigma_{2}\), \(\exists\sigma_{1},\sigma_{2}\in\mathcal{P}\cup\{\bot\},\forall x\in\mathcal{P}\)) and the learner gathers \(f+1\) votes (i.e., \(min\_accepted(s,b)\)). The first case requires gathering \(N-f\) votes from each acceptor and validating that each proof corresponds to the correct ballot and value (Algorithm 10, lines [1-12]). The second case requires that the sequence must be commutative with any other and at least \(f+1\) matching values are gathered (Algorithm 10, [14-18]).