560 lines
39 KiB
TeX
560 lines
39 KiB
TeX
|
|
\subsection{Model extension}
|
|
We extend the crash model of Section 1 (same process universe, asynchronous setting, uniquely identifiable messages, and reliable point-to-point channels) with Byzantine faults and Byzantine-resilient dissemination primitives.
|
|
|
|
\paragraph{Failure threshold.} At most $t$ processes may be Byzantine, and we assume $n > 3t$, following standard asynchronous Byzantine assumptions~\cite{Bracha87}.
|
|
|
|
\paragraph{Additional communication primitive.} In addition to reliable point-to-point channels, processes use Reliable Broadcast ($\RB$) with operations $\RBcast(m)$ and $m=\rdeliver()$. We use Bracha's Byzantine RB specification~\cite{Bracha87}: for a fixed sender and broadcast instance, all correct processes that deliver, deliver the same payload, and Byzantine equivocation on that instance is prevented.
|
|
|
|
\paragraph{Byzantine behaviour}
|
|
A Byzantine process may deviate arbitrarily from the algorithm (malformed inputs, selective omission, collusion, inconsistent timing, etc.).
|
|
|
|
Byzantine processes are still constrained by the assumed primitives: they cannot violate the safety/liveness guarantees of $\DL$ and cannot break the Integrity, No-duplicates, and Validity guarantees of $\RB$.
|
|
|
|
|
|
\paragraph{Notation.} For any indice $k$ we defined by $\DL[k]$ as the $k$-th DenyList object. For a given $\DL[k]$ and any indice $x$ we defined by $\Pi_x^k$ a subset of $\Pi$. Still for a given $k$ we consider $\Pi_M^k \subseteq \Pi$ and $\Pi_V^k \subseteq \Pi$ two authorization subsets for $\DL[k]$. Indice $i \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec_k$ for the $\DL[k]$ linearization: $x \prec_k y$ means that operation $x$ appears strictly before $y$ in the linearized history of $\DL[k]$. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes).
|
|
For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked by process $p_i$, and by $F_i^k(...)$ the same operation invoked on the $\DL[k]$ object.
|
|
|
|
% ------------------------------------------------------------------------------
|
|
\subsection{Primitives}
|
|
|
|
\subsection{Reliable Broadcast (RB)}
|
|
|
|
\RB provides the following properties in this model (cf.~\cite{Bracha87}).
|
|
\begin{itemize}[leftmargin=*]
|
|
\item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ m = \rbreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$.
|
|
\item \textbf{No-duplicates}: No message is received more than once at any process.
|
|
\item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
|
|
\end{itemize}
|
|
|
|
\subsubsection{t-BFT-DL}
|
|
|
|
We consider a t-Byzantine Fault Tolerant DenyList (t-$\BFTDL$) with the following properties.
|
|
There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD()$ such that :
|
|
|
|
\paragraph{Termination.} Every operation $\BFTAPPEND(x)$, $\BFTPROVE(x)$, and $\BFTREAD()$ invoked by a correct process always returns.
|
|
|
|
\paragraph{PROVE Validity.} The invocation of $op = \BFTPROVE(x)$ by a correct process is valid iff there exist a set of correct process $C$ such that $\forall c \in C$, $c$ invoke $op_2 = \BFTAPPEND(x)$ with $op_2 \prec op_1$ and $|C| \leq t$
|
|
|
|
\paragraph{PROVE Anti-Flickering.} If the invocation of a operation $op = \BFTPROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\BFTPROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
|
|
|
|
\paragraph{READ Liveness.} Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, x) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$.
|
|
|
|
\paragraph{READ Anti-Flickering.} Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$.
|
|
|
|
\paragraph{READ Safety.} Let $op_1, op_2$ respectively a valid $\BFTPROVE(x)$ operation submited by the process $p_i$ and a $\BFTREAD()$ operation submited by any correct process such that $op_1 \prec op_2$. Let $R$ the result of $op_2$ then $R \ni (i, x)$
|
|
|
|
\subsection{DL $\Rightarrow$ t-BFT-DL}
|
|
|
|
|
|
Fix $3t < |M|$. Let
|
|
\[
|
|
\mathcal{U} = \{\, U \subseteq M \mid |U| = |M| - t \,\}.
|
|
\]
|
|
For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose authorization sets are
|
|
\[
|
|
\Pi_M(DL_T) = S_T = U
|
|
\qquad\text{and}\qquad
|
|
\Pi_V(DL_T) = V.
|
|
\]
|
|
|
|
\[
|
|
|\mathcal{U}| = \binom{|M|}{|M| - t}.
|
|
\]
|
|
|
|
\begin{algorithm}
|
|
\caption{t-BFT-DL implementation using multiple DL objects}
|
|
|
|
\Fn{$\BFTAPPEND(x)$}{
|
|
\For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$}{
|
|
$DL_U.\APPEND(x)$\;
|
|
}
|
|
}
|
|
|
|
\vspace{1em}
|
|
|
|
\Fn{$\BFTPROVE(x)$}{
|
|
$\state \gets false$\;
|
|
\For{\textbf{each } $U \in \mathcal{U}$}{
|
|
$\state \gets \state \textbf{ OR } DL_U.\PROVE(x)$\;\nllabel{code:prove-or}
|
|
}
|
|
\Return{$\state$}\;
|
|
}
|
|
|
|
\vspace{1em}
|
|
|
|
\Fn{$\BFTREAD()$}{
|
|
$\results \gets \emptyset$\;
|
|
\For{\textbf{each } $U \in \mathcal{U}$}{
|
|
$\results \gets \results \cup DL_U.\READ()$\;
|
|
}
|
|
\Return{$\results$}\;
|
|
}
|
|
\end{algorithm}
|
|
|
|
\paragraph{Algorithm intuition.}
|
|
In the Byzantine setting, a process identifier $j$ is selected in $\winners[r]$ only when it accumulates at least $t+1$ proofs for round $r$ in $\validated(r)$. A process emits such a proof for $j$ only after receiving $j$'s $\texttt{PROP}$ payload (handler $\rdeliver(\texttt{PROP},\cdot)$). Therefore, if $j$ is a winner, at least one correct process has received $j$'s proposal. By RB agreement/validity, once one correct process receives that proposal for the instance, all correct processes eventually receive the same payload, so winner proposals eventually become available everywhere and can be merged consistently.
|
|
|
|
\begin{lemma}[BFT-PROVE Validity]\label{lem:bft-prove-validity}
|
|
The invocation of $op = \BFTPROVE(x)$ by a correct process is invalid iff there exist at least $t+1$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$. Let $A\subseteq M$ be the set of distinct issuers that invoked $\BFTAPPEND(x)$ before $op$ in $\Seq$.
|
|
|
|
\begin{itemize}
|
|
\item \textbf{Case (i): $|A|\ge t+1$.}
|
|
Fix any $U\in\mathcal{U}$. $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND_j(x)$ triggers $DL_U.\APPEND(x)$, and because $\BFTAPPEND_j(x)\prec op$ in $\Seq$, this induces a valid $DL_U.\APPEND(x)$ that appears before the induced $DL_U.\PROVE(x)$ by $p_i$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $U\in\mathcal{U}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so the field $\state$ at line~\ref{code:prove-or} is never becoming true, and $op$ return false.
|
|
|
|
\item \textbf{Case (ii): $|A|\le t$.}
|
|
There exists $U^\star\in\mathcal{U}$ such that $A\cap U^\star=\emptyset$. For any $j\in A$, we have $j\notin U^\star$, so $\BFTAPPEND_j(x)$ does \emph{not} call $DL_{U^\star}.\APPEND(x)$. Hence no valid $DL_{U^\star}.\APPEND(x)$ appears before the induced $DL_{U^\star}.\PROVE(x)$. Since also $i\in \Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE(x)$ is valid. Therefore, there exists a component with a valid $\PROVE(x)$, so $op$ is valid.
|
|
\end{itemize}
|
|
|
|
\smallskip
|
|
Combining the cases yields the claimed characterization of invalidity.
|
|
\end{proof}
|
|
|
|
\begin{lemma}[BFT-PROVE Anti-Flickering]\label{lem:bft-prove-anti-flickering}
|
|
If the invocation of a operation $op = \BFTPROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\BFTPROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$ that is \emph{invalid} in $\Seq$.
|
|
By BFT-PROVE Validity, this implies that there exist at least $t+1$ \emph{distinct} processes in $M$ that invoked a \emph{valid} $\BFTAPPEND(x)$ before $op$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\ge t+1$.
|
|
|
|
Fix any $U\in\mathcal{U}$. We have $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND_j(x)$ triggers a call $DL_U.\APPEND(x)$. Moreover, because $\BFTAPPEND_j(x)\prec op$ in $\Seq$, the induced $DL_U.\APPEND(x)$ appears before the induced $DL_U.\PROVE(x)$ of $op$ in the projection $\Seq_U$.
|
|
|
|
Hence, in $\Seq_U$, there exists a \emph{valid} $DL_U.\APPEND(x)$ that appears before the $DL_U.\PROVE(x)$ induced by $op$. By \textbf{PROVE Validity} the base $\DL$ object, the induced $DL_U.\PROVE(x)$ is therefore \emph{invalid} in $\Seq_U$.
|
|
|
|
Let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $U\in\mathcal{U}$. Hence, the $DL_U.\PROVE(x)$ induced by $op'$ appears after the $DL_U.\PROVE(x)$ induced by $op$ in $\Seq_U$. Since the induced $DL_U.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_U.\PROVE(x)$ in $\Seq_U$ is invalid.
|
|
|
|
As this holds for every $U\in\mathcal{U}$, there is no component $DL_U$ in which the induced $\PROVE(x)$ of $op'$ is valid.
|
|
\end{proof}
|
|
|
|
\begin{lemma}[BFT-READ Liveness]
|
|
Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, x) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $R$ the result of a $READ()$ operation submit by any correct process. $(i, x) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, x) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, x) \in R^{U^\star}$ implie that there exist a valid $DL_{U^\star}.\PROVE_i(x)$. The for loop in the $\BFTPROVE(x)$ implementation return true iff there at least one valid $DL_{U}.\PROVE_i(x)$ for any $U \in \mathcal{U}$.
|
|
|
|
Hence because there exist a $U^\star$ such that $DL_{U^\star}.\PROVE_i(x)$, there exist a valid $\BFTPROVE_i(x)$.
|
|
|
|
$(i, x) \in R \implies \exists \BFTPROVE_i(x)$
|
|
\end{proof}
|
|
|
|
\begin{lemma}[BFT-READ Anti-Flickering]\label{lem:bft-read-anti-flickering}
|
|
Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $R_1, R_2$ respectively the output of two $\BFTREAD()$ operations $op_1, op_2$ such that $op_1 \prec op_2$.
|
|
By the implementation of $\BFTREAD$, $R_k = \bigcup_{U \in \mathcal{U}} R_k^U$ where $R_k^U$ is the result of $DL_U.\READ()$ during $op_k$.
|
|
|
|
Because $op_1 \prec op_2$ for any $U \in \mathcal{U}$, the $DL_U.\READ()$ induced by $op_1$ happen before the $DL_U.\READ()$ induced by $op_2$. Hence we have for all $U, R_2^U \subseteq R_1^U$.
|
|
Therefore
|
|
\[
|
|
\bigcup_U R_2^U \subseteq \bigcup_U R_1^U \implies
|
|
R_2 \subseteq R_1
|
|
\]
|
|
\end{proof}
|
|
|
|
\begin{lemma}[BFT-READ Safety]\label{lem:bft-read-safety}
|
|
Let $op_1, op_2$ respectively a valid $\BFTPROVE(x)$ operation submited by the process $p_i$ and a $\BFTREAD()$ operation submited by any correct process such that $op_1 \prec op_2$. Let $R$ the result of $op_2$ then $R \ni (i, x)$
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $op_1 = \BFTPROVE_i(x)$ be a valid operation by a correct process $p_i$ and $op_2 = \BFTREAD()$ be any $\BFTREAD()$ operation such that $op_1 \prec op_2$ in $\Seq$.
|
|
By BFT-PROVE Validity, there exist at most $t$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op_1$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\le t$.
|
|
|
|
There exists $U^\star\in\mathcal{U}$ such that $A\cap U^\star=\emptyset$. For any $j\in A$, we have $j\notin U^\star$, so $\BFTAPPEND^{(j)}(x)$ does \emph{not} call $DL_{U^\star}.\APPEND(x)$. Hence no valid $DL_{U^\star}.\APPEND(x)$ appears before the induced $DL_{U^\star}.\PROVE(x)$ of $op_1$. Since also $i\in \Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE_i(x)$ is valid.
|
|
|
|
Now, because $op_1 \prec op_2$ in $\Seq$, the induced $DL_{U^\star}.\PROVE_i(x)$ appears before the induced $DL_{U^\star}.\READ()$ of $op_2$ in $\Seq_{U^\star}$. By \textbf{READ Safety} of $\DL$, the result $R^{U^\star}$ of the induced $DL_{U^\star}.\READ()$ contains $(i, x)$.
|
|
|
|
Finally, by the implementation of $\BFTREAD()$, we have $R = \bigcup_{U \in \mathcal{U}} R^U$, so $(i, x) \in R$.
|
|
\end{proof}
|
|
|
|
\begin{theorem}
|
|
For any fixed value $t$ such that $3t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
|
|
\end{theorem}
|
|
|
|
\begin{proof}
|
|
Follows directly from the previous lemmas.
|
|
\end{proof}
|
|
|
|
\subsection{Algorithm}
|
|
|
|
\begin{algorithm}[H]
|
|
\caption{t-BFT ARB at process $p_i$}\label{alg:bft-arb}
|
|
|
|
\SetKwBlock{LocalVars}{Local Variables:}{}
|
|
\LocalVars{
|
|
$\unordered \gets \emptyset$,
|
|
$\ordered \gets \epsilon$,
|
|
$\delivered \gets \epsilon$\;
|
|
$\prop[r][j] \gets \bot, \forall j, r \in \Pi \times \mathbb{N}$\;
|
|
$\done[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
|
|
}
|
|
|
|
\vspace{0.3em}
|
|
|
|
\For{$r = 1, 2, \ldots$}{\nllabel{alg:main-loop}
|
|
\textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
|
|
$S \gets \unordered \setminus \ordered$;
|
|
$\RBcast(\texttt{PROP}, S, \langle i, r \rangle)$\;
|
|
|
|
\textbf{wait until} $|\validated(r)| \geq n - t$\;\nllabel{alg:check-validated}
|
|
|
|
\BlankLine
|
|
|
|
\lForEach{$j \in \Pi$}{
|
|
$\BFTAPPEND(\langle j, r\rangle)$\nllabel{alg:append}
|
|
}
|
|
|
|
\lForEach{$j \in \Pi$}{
|
|
$\send(\texttt{DONE}, r)$ \textbf{ to } $p_j$
|
|
}
|
|
|
|
\BlankLine
|
|
|
|
\textbf{wait until} $|\done[r]| \geq n - t$\;\nllabel{alg:check-done}
|
|
\textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$ \textbf{ with } $\winners[r] \gets \validated(r)$\;
|
|
|
|
\BlankLine
|
|
|
|
$M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
|
|
$\ordered \gets \ordered \cdot \order(M)$\;
|
|
}
|
|
|
|
\vspace{0.3em}
|
|
|
|
\Fn{\validated($r$)}{
|
|
\Return{$\{j: |\{k: (k, r) \in \BFTREAD()\}| \geq t+1\}$}\;
|
|
}
|
|
|
|
\vspace{0.3em}
|
|
|
|
\Upon{$\ABbroadcast(m)$}{
|
|
$\unordered \gets \unordered \cup \{m\}$\;
|
|
}
|
|
|
|
\vspace{0.3em}
|
|
|
|
\Upon{$\rdeliver(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
|
|
$\unordered \gets \unordered \cup S$;
|
|
$\prop[r][j] \gets S$\;
|
|
$\BFTPROVE(\langle j, r\rangle)$\;
|
|
}
|
|
|
|
\vspace{0.3em}
|
|
|
|
\Upon{$\receive(\texttt{DONE}, r)$ from process $p_j$}{
|
|
$\done[r] \gets \done[r] \cup \{j\}$\;
|
|
}
|
|
|
|
\vspace{0.3em}
|
|
|
|
\Upon{$\ABdeliver()$}{
|
|
\lIf{$\ordered \setminus \delivered = \emptyset$}{
|
|
\Return{$\bot$}
|
|
}
|
|
let $m$ be the first message in $(\ordered \setminus \delivered)$\;
|
|
$\delivered \gets \delivered \cdot \{m\}$\;
|
|
\Return{$m$}
|
|
}
|
|
|
|
\end{algorithm}
|
|
|
|
\paragraph{Algorithm intuition.}
|
|
The Byzantine-tolerant construction combines threshold evidence and RB agreement to make winner selection robust. A sender $j$ appears in $\validated(r)$ only when at least $t+1$ proofs for $\langle j,r\rangle$ are observed through $\BFTREAD()$, and by \Cref{lem:bft-prove-validity} this threshold means that $j$ cannot be certified without broad enough support from the system. Once a round is closed, the winner set becomes stable by \Cref{lem:winners-stability}, so correct processes stop diverging on who contributes to the round outcome. For each stable winner, the associated proposal payload is unique at correct receivers by \Cref{lem:bft-unique-proposal}, which prevents equivocation from creating distinct local values for the same winner identity. Consequently, when correct processes wait for all winner proposals and compute the union at line~\ref{code:Mcompute}, they obtain the same message set by \Cref{lem:message-content-invariance}. Progress is then ensured by \Cref{lem:bft-eventual-closure}, which guarantees that if new messages remain unordered, a new round eventually closes with at least $n-t$ winners. Finally, once rounds are commonly closed, appending $\order(M)$ at each round yields a common delivery sequence, exactly formalized by \Cref{lem:bft-total-order}.
|
|
|
|
% \textbf{Everything below has to be updated}
|
|
|
|
% \begin{definition}[BFT Closed round for $k$]
|
|
% Given $Seq^{k}$ the linearization of the $\BFTDL$ $Y[k]$, a round $r \in \mathcal{R}$ is \emph{closed} in $\Seq$ iff there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. Let call $\BFTAPPEND(r)^\star$ the $(n-f)^{th}$ $\BFTAPPEND(r)$.
|
|
% \end{definition}
|
|
|
|
% \begin{definition}[BFT Closed round]\label{def:bft-closed-round}
|
|
% A round $r \in \mathcal{R}$ is \emph{closed} iff for all $\DL[k]$, $r$ is closed in $\Seq^k$.
|
|
% \end{definition}
|
|
|
|
% \subsection{Proof of correctness}
|
|
|
|
% \begin{remark}[BFT Stable round closure]\label{rem:bft-stable-round-closure}
|
|
% If a round $r$ is closed, no more $\BFTPROVE(r)$ can be valid and thus linearized. In other words, once $\BFTAPPEND(r)^\star$ is linearized, no more process can make a proof on round $r$, and the set of valid proofs for round $r$ is fixed. Therefore $\Winners_r$ is fixed.
|
|
% \end{remark}
|
|
|
|
% \begin{proof}
|
|
% By definition $r$ closed means that for all process $p_i$, there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. By BFT-PROVE Validity, any subsequent $\BFTPROVE(r)$ is invalid because at least $n - f$ processes already invoked a valid $\BFTAPPEND(r)$ before it. Thus no new valid $\BFTPROVE(r)$ can be linearized after $\BFTAPPEND(r)^\star$. Hence the set of valid proofs for round $r$ is fixed, and so is $\Winners_r$.
|
|
% \end{proof}
|
|
|
|
% \begin{lemma}[BFT Across rounds]\label{lem:bft-across-rounds}
|
|
% For any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
|
|
% \end{lemma}
|
|
|
|
% \begin{proof}
|
|
% Let $r \in \mathcal{R}$. By \cref{def:bft-closed-round}, if $r + 1$ is closed, then for all $\DL[k]$, $r + 1$ is closed in $\Seq^k$. By the implementation, a process can only invoke $\BFTAPPEND(r + 1)$ after observing at least $n - f$ valid $\BFTPROVE(r)$, which means that for all $\DL[k]$, $r$ is closed in $\Seq^k$. Hence by \cref{def:bft-closed-round}, $r$ is closed.
|
|
|
|
% Because $r$ is monotonically increasing, we can reccursively apply the same argument to conclude that for any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
|
|
% \end{proof}
|
|
|
|
% \begin{lemma}[BFT Progress]\label{lem:bft_progress}
|
|
% For any correct process $p_i$ such that
|
|
% \[
|
|
% \received \setminus (\delivered \cup (\cup_{r' < r} \cup_{j \in W[r'] \prop[r'][j]})) \neq \emptyset
|
|
% \]
|
|
% with $r$ the highest closed round in the $\DL$ linearization. Eventually $r+1$ will be closed.
|
|
% \end{lemma}
|
|
|
|
% \begin{lemma}[BFT Winners invariant]\label{lem:bft-winners-invariant}
|
|
% For any closed round $r$, define
|
|
% \[
|
|
% \Winners_r = \{j: \BFTPROVE_j(r) \prec \BFTAPPEND^\star(r)\}
|
|
% \]
|
|
% called the unique set of winners of round $r$.
|
|
% \end{lemma}
|
|
|
|
% \begin{lemma}[BFT n-f lower-bounded Winners]
|
|
% Let $r$ a closed round, $|W[r]| \geq n-f$.
|
|
% \end{lemma}
|
|
|
|
% \begin{remark}\label{rem:correct-in-winners}
|
|
% Because we assume $n \geq 2f+ 1$, if $|W[r]| \geq n-f$ at least 1 correct have to be in $W[r]$ to progress.
|
|
% \end{remark}
|
|
|
|
% \begin{lemma}[BFT Winners must purpose]\label{lem:bft-winners-purpose}
|
|
% Let $r$ a closed round, for all process $p_j$ such that $j \in W[r]$, $p_j$ must have executed $\RBcast(j, PROP, \_, r)$ and hence any correct will eventually set $\prop[r][j]$ to a non-$\bot$ value.
|
|
% \end{lemma}
|
|
|
|
% \begin{lemma}[BFT Messages Incariant]\label{lem:bft-messages-invariant}
|
|
% For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r$: $\prop^{(i)}[r][j] \neq \bot$ define
|
|
% \[
|
|
% \Messages_r = \cup_{j \in \Winners_r} prop^{(i)}[r][j]
|
|
% \]
|
|
% as the set of messages proposed by the winners of round $r$
|
|
% \end{lemma}
|
|
|
|
% \begin{lemma}[BFT EVentual proposal closure]\label{lem:bft-eventual-proposal-closure}
|
|
% If a correct process $p_i$ define $M$ at line~\ref{code:Mcompute}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
|
|
% \end{lemma}
|
|
|
|
% \begin{lemma}[BFT Unique proposal per sender per round]\label{lem:bft-unique-proposal}
|
|
% For any round $r$ and any process $p_i$, if $p_i$ invokes two $\RBcast$ call for the same round, such that $\RBcast(i, PROP, S, r) \prec \RBcast(i, PROP, S', r)$. Then for any correct process $p_j$, $\prop^{(j)}[r][i] \in \{\bot, S\}$
|
|
% \end{lemma}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
% \begin{lemma}[BFT $W_r$ as grow only set]\label{lem:bft-wr-grow-only}
|
|
% For any correct process $p_i$. If $p_i$ computes $W_r$ at two different times $t_1$ and $t_2$ with $t_1 < t_2$, then $W_r^{t_1} \subseteq W_r^{t_2}$.
|
|
% \end{lemma}
|
|
|
|
% \begin{proof}
|
|
% By the implementation, $W_r$ is computed exclusively from the results of $\{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$.
|
|
|
|
% We know by BFT-READ Anti-Flickering that for any two $\BFTREAD()$ operations $op_1, op_2$ such that $op_1 \prec op_2$, the result of $op_2$ is included in the result of $op_1$. Therefore, if $p_i$ computes $W_r$ at two different times $t_1$ and $t_2$ with $t_1 < t_2$, then $W_r^{t_1} \subseteq W_r^{t_2}$.
|
|
% \end{proof}
|
|
|
|
% \begin{lemma}[BFT well defined winners]\label{lem:bft-well-defined-winners}
|
|
% For any closed round $r$, if a correct process $p_i$ compute $W_r$, then $W_r = \Winners_r$ with $|W_r| \geq n - f$.
|
|
% \end{lemma}
|
|
|
|
% \begin{proof}
|
|
% By \Cref{lem:bft-read-safety}, any correct process $p_i$ computing $W_r$ after round $r$ is closed includes all valid $\BFTPROVE(r)$ in its computation of $W_r$. Therefore $W_r = \Winners_r$.
|
|
|
|
% By \Cref{def:bft-closed-round}, at least $n - f$ distinct processes invoked a valid $\BFTAPPEND(r)$ before $\BFTAPPEND(r)^\star$. By the implementation in algorithm D, if a process correct $j$ invoked a valid $\BFTAPPEND(r)$, thats means that he observed at least $n - f$ valid $\BFTPROVE(r)$ submitted by distinct processes. By \Cref{lem:bft-wr-grow-only}, once $p_j$ observed $n - f$ valid $\BFTPROVE(r)$, any correct process computing $W_r$ will eventually observe at least these $n - f$ valid $\BFTPROVE(r)$. By \Cref{lem:bft-stable-round-closure}, no more valid $\BFTPROVE(r)$ can be linearized after round $r$ is closed, so any correct process computing the same fixed set $W_r$ of at least $n - f$ distinct processes.
|
|
% \end{proof}
|
|
|
|
% \begin{lemma}[BFT Non-empty winners proposal]\label{lem:bft-non-empty-winners-proposal}
|
|
% For every process $p_i$ such as $i \in W_r$, eventually $\prop[r][i] \neq \bot$.
|
|
% \end{lemma}
|
|
|
|
% \begin{proof}
|
|
% By the implementation, if $i \in W_r$, then $(i, \PROVEtrace(r))$ is included in the result of at least one $\BFTREAD()$ operation. Hence there exist a valid $\BFTPROVE(r)$ operation.
|
|
% By \Cref{lem:bft-prove-validity}, this implies that there exist at least $f + 1$ valid $\PROVE(r)$ operation invoked by processes. At least one of these processes is correct, say $p_j$. By the implementation, $p_j$ invoked $\BFTPROVE(r)$ after receiving a $Rdeliver(j, \texttt{PROP}, S, r)$ message from $p_i$. Therefore, by the reliable broadcast properties, the message will eventually be delivered to every correct process, hence eventually for any correct process $\prop[r][i] \neq \bot$.
|
|
% \end{proof}
|
|
|
|
% \begin{definition}[BFT Message invariant]\label{def:bft-message-invariant}
|
|
% For any closed round $r$, for any correct process $p_i$, such that $\nexists j \in W_r : \prop[r][j] = \bot$, twe define the set
|
|
% \[
|
|
% \Messages_r = \bigcup_{j \in \Winners_r} \prop[r][j]
|
|
% \]
|
|
% as the unique set of messages proposed during round $r$.
|
|
% \end{definition}
|
|
|
|
% \begin{lemma}[BFT Proposal convergence]\label{lem:bft-proposal-convergence}
|
|
% For any closed round $r$, for any correct process $p_i$, that define $M_r$ at line B10, we have $M_r = \Messages_r$.
|
|
% \end{lemma}
|
|
|
|
% \begin{proof}
|
|
% By \Cref{lem:bft-well-defined-winners}, any correct process $p_i$ computing $W_r$ after round $r$ is closed has $W_r = \Winners_r$.
|
|
% By \Cref{lem:bft-non-empty-winners-proposal}, for any correct process $p_i$, such as $i \in W_r$, eventually $\prop[r][i] \neq \bot$.
|
|
|
|
% Therefore, eventually for any correct process $p_i$, at line B10 we have
|
|
% \[
|
|
% M_r = \bigcup_{j \in W_r} \prop[r][j] = \bigcup_{j \in \Winners_r} \prop[r][j] = \Messages_r
|
|
% \]
|
|
% \end{proof}
|
|
|
|
% \begin{lemma}[BFT Inclusion]\label{proof:bft-inclusion}
|
|
% If a correct process $p_i$ ABroadcasts a message $m$, then eventually any correct process $p_j$ ADelivers $m$.
|
|
% \end{lemma}
|
|
|
|
% \begin{proof}
|
|
% Let $m$ be a message ABroadcast by a correct process $p_i$ and eventually exit the \texttt{ABroadcast} function at line A10.
|
|
|
|
% By the implementation, if $p_i$ exits the \texttt{ABroadcast} function at line A10, then there exists a round $r'$ such that $m \in \prop[r'][j]$ for some $j \in W_{r'}$.
|
|
|
|
% Since $p_i$ is correct, seeing that $m \in \prop[r'][j]$ for some $j \in W_{r'}$ implies that $p_i$ received a $Rdeliver(j, \texttt{PROP}, S, r')$ message from $p_j$ such that $m \in S$. And because $p_j$ is in $W_{r'}$, at least $n - f$ correct processes invoked a valid $Y[j].\BFTPROVE(r')$ before the round $r'$ were closed. By the reliable broadcast properties, the $Rdeliver(j, \texttt{PROP}, S, r')$ message will eventually be delivered to every correct process, hence eventually for any correct process $m \in \prop[r'][j]$ with $j \in W_{r'}$. Hence $m$ will eventually be included in the set $\Messages_{r'}$ defined in \Cref{def:bft-message-invariant} and thus eventually be ADelivered by any correct process.
|
|
% \end{proof}
|
|
|
|
\subsection{Correctness Lemmas}
|
|
|
|
\begin{definition}[Closed Round]
|
|
A round $r \in \mathcal{R}$ is said to be \emph{closed} for a correct process $p_i$ if at the moment $p_i$ computes $\winners[r]$, it satisfies $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$.
|
|
\end{definition}
|
|
|
|
\begin{lemma}[Round Monotonicity]\label{lem:round-monotonicity}
|
|
If a round $r$ is closed, then every round $r_1 < r$ is also closed.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
\textbf{Base:} $r = 0$. Suppose round $1$ is closed, the set $\{r' \in \mathcal{R}: r' < r\}$ is empty, so the claim holds.
|
|
|
|
\textbf{Inductive step:} Let $r \geq 1$. Assume that the property holds for all rounds $r' < r$: whenever round $r'$ is closed, all rounds $r_2 < r'$ are also closed. We show that if round $r$ is closed, then all rounds $r_1 < r$ are closed.
|
|
|
|
Suppose round $r$ is closed. This means at least one correct process $p_i$ has reached line \ref{alg:check-validated} and satisfied the condition $|\validated(r)| \geq n - t$. Consequently, $p_i$ has invoked $\BFTAPPEND(\langle j, r \rangle)$ for each $j \in \Pi$ at line \ref{alg:append}. Since these operations are invoked by a correct process, and they depend on valid proofs in the byzantine fault tolerant deny list, at least one of these operations must have succeeded in the DL object.
|
|
|
|
Moreover, by the algorithm structure, a correct process can only reach the beginning of round $r$ after completing round $r-1$. In particular, process $p_i$ reaches line \ref{alg:main-loop} for round $r$ only after having completed round $r-1$, which requires the process to have observed at least $|\done[r-1]| \geq n - t$ (line \ref{alg:check-done} for round $r-1$). This condition can only be satisfied if round $r-1$ is closed: at least $n - t$ processes must have issued DONE messages, and since $n > 3f$, at least one of these is correct.
|
|
|
|
Since $n - t > 2f + 1$, among the $n - t$ processes satisfying the condition for round $r-1$, at least one is correct. A correct process that issued a DONE message for round $r-1$ must have previously completed its execution of lines \ref{alg:append} for round $r-1$, which in turn required observing $|\validated(r-1)| \geq n - t$ from line \ref{alg:check-validated}. Thus, round $r-1$ is closed.
|
|
|
|
Now, considering any round $r_1 < r-1$: by the inductive hypothesis applied to round $r-1$, since round $r-1$ is closed and $r_1 < r-1$, we have that $r_1$ is also closed.
|
|
|
|
By strong induction, if round $r$ is closed, all rounds $r_1 < r$ are closed.
|
|
\end{proof}
|
|
|
|
\begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:bft-unique-proposal}
|
|
For any closed round $r$ and any process $p_j \in \winners[r]$, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process $p_i$ that has received a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly this set $S_j$.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $r$ be a closed round and $p_j \in \winners[r]$. Since $j \in \winners[r]$, it means that $(j, r) \in \BFTREAD()$, i.e., at least $t+1$ distinct processes have invoked a valid $\BFTPROVE(\langle j, r \rangle)$ before the round $r$ closed.
|
|
|
|
By the algorithm, a correct process $p_i$ invokes $\BFTPROVE(\langle j, r \rangle)$ only upon receiving a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ at line \ref{alg:append}. Let $S_j^{(i)}$ denote the set received by $p_i$.
|
|
|
|
Since at least $t+1$ distinct processes have performed a valid $\BFTPROVE(\langle j, r \rangle)$, and since $t < n/3$, at least one of these processes is correct. Thus, at least one correct process must have received a reliable broadcast from $p_j$ for round $r$.
|
|
|
|
Now, by Bracha's Byzantine Reliable Broadcast specification, for any message broadcast instance by process $p_j$ in round $r$, all correct processes that deliver this broadcast either receive the identical message or none at all. Formally, for all correct processes $p_i, p_i'$ that received a delivery from $p_j$ for round $r$, we have $S_j^{(i)} = S_j^{(i')}$.
|
|
|
|
Therefore, there exists a unique set $S_j$ such that every correct process $p_i$ that receives a reliable delivery from $p_j$ for round $r$ receives exactly $S_j$.
|
|
\end{proof}
|
|
|
|
\begin{lemma}[Winners Stability]\label{lem:winners-stability}
|
|
For any closed round $r$, the set $\winners[r]$ is stable.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $r$ be a closed round. By definition, a closed round $r$ means that at least one correct process $p_i$ has observed $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$ and computed $\winners[r]$ at line \ref{alg:check-done}.
|
|
|
|
When round $r$ becomes closed, this implies that at least $n - t$ distinct processes have invoked $\BFTAPPEND(\langle j, r \rangle)$ for $j \in \Pi$ (by the algorithm structure, since $\done[r]$ contains DONE messages from processes that completed line \ref{alg:append}). Since $n > 3f$, we have $n - t > 2f + 1 > t + 1$.
|
|
|
|
Consider a fixed $j \in \Pi$. Since at least $n - t > t + 1$ processes have invoked a valid $\BFTAPPEND(\langle j, r \rangle)$, by \cref{lem:bft-prove-validity}, any subsequent invocation of $\BFTPROVE(\langle j, r \rangle)$ will be invalid.
|
|
|
|
By \cref{lem:bft-prove-anti-flickering}, once a $\BFTPROVE(\langle j, r \rangle)$ operation becomes invalid, all subsequent $\BFTPROVE(\langle j, r \rangle)$ operations are also invalid.
|
|
|
|
This holds for all $j \in \Pi$. Therefore, after the round $r$ is closed, the set of valid $\BFTPROVE(\langle j, r \rangle)$ operations for each $j$ cannot grow. By \cref{lem:bft-read-anti-flickering}, any subsequent $\BFTREAD()$ invocation will not return any new $(k, r)$ pairs beyond those already returned. Thus, $\winners[r] = \{j : (j, r) \in \BFTREAD()\}$ becomes stable and cannot change.
|
|
|
|
Since this reasoning applies to all correct processes that compute $\winners[r]$ after round $r$ is closed, all correct processes will compute the same stable set $\winners[r]$.
|
|
\end{proof}
|
|
|
|
\begin{lemma}[Message Content Invariance]\label{lem:message-content-invariance}
|
|
For any closed round $r$ and any correct process $p_i$, the set $M$ computed at line \ref{code:Mcompute} by $p_i$ is identical to the set computed by any other correct process $p_j$ for the same round $r$.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $r$ be a closed round and let $p_i, p_{i'}$ be two correct processes. By the algorithm, both processes compute $M$ as:
|
|
\[
|
|
M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j]
|
|
\]
|
|
and
|
|
\[
|
|
M^{(i')} = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j]
|
|
\]
|
|
at line \ref{code:Mcompute}.
|
|
|
|
By \cref{lem:winners-stability}, the set $\winners[r]$ is stable once round $r$ is closed. Therefore, both $p_i$ and $p_{i'}$ compute the same set of winners $\winners[r]$.
|
|
|
|
Now, consider any winner $j \in \winners[r]$. By \cref{lem:bft-unique-proposal}, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process that receives a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly $S_j$.
|
|
|
|
By the algorithm, each correct process stores this received set in its local variable: $\prop^{(i)}[r][j] = S_j$ and $\prop^{(i')}[r][j] = S_j$.
|
|
|
|
Since both processes compute the union over the same set of winners, and each winner's proposal is identical for all correct processes:
|
|
\[
|
|
M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j] = \bigcup_{j \in \winners[r]} S_j = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j] = M^{(i')}
|
|
\]
|
|
|
|
Therefore, all correct processes compute the same set $M$ for any closed round $r$.
|
|
\end{proof}
|
|
|
|
\begin{lemma}[Inclusion]\label{lem:bft-inclusion}
|
|
If a correct process $p_i$ invokes $\ABbroadcast(m)$, then there exist a closed round $r$ and a winner $j \in \winners[r]$ such that $p_j$ invoked $\RBcast(j, \texttt{PROP}, S, r)$ with $m \in S$.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the algorithm, $p_i$ adds $m$ to $\unordered$. Consequently, $\unordered \setminus \ordered \neq \emptyset$, and the process enters the main loop and eventually invokes $\RBcast(i, \texttt{PROP}, S_i^{(1)}, r_1)$ for some round $r_1$ where $m \in S_i^{(1)}$.
|
|
|
|
We distinguish two cases:
|
|
|
|
\textbf{Case 1: $p_i$ becomes a winner in round $r_1$.}
|
|
If $p_i$ is elected as a winner for round $r_1$ (i.e., $i \in \winners[r_1]$), then the claim holds with $r = r_1$ and $j = i$.
|
|
|
|
\textbf{Case 2: $p_i$ does not become a winner in round $r_1$.}
|
|
If $p_i$ is not elected as a winner, by the properties of Reliable Broadcast (Bracha's specification), at least one correct process $p_{i_1}$ will eventually receive the reliable delivery of the $\texttt{PROP}$ message from $p_i$ for round $r_1$. Process $p_{i_1}$ adds all messages from $S_i^{(1)}$ to its $\unordered$ set at line \ref{alg:append}. In particular, $m$ is now in $p_{i_1}$'s $\unordered$ set.
|
|
|
|
In round $r_2 > r_1$ (and any subsequent round), process $p_{i_1}$ computes $S_{i_1}^{(2)} = \unordered \setminus \ordered$ and invokes $\RBcast(i_1, \texttt{PROP}, S_{i_1}^{(2)}, r_2)$ with $m \in S_{i_1}^{(2)}$.
|
|
|
|
This process repeats: either $p_{i_1}$ becomes a winner and the claim holds, or another correct process receives $p_{i_1}$'s proposal and includes $m$ in its own proposal.
|
|
|
|
Since $n > 3f$, we have $n - t > t + 1 > f$. By the pigeonhole principle, there eventually exists a round $r$ where at least $n - t$ distinct processes have proposed sets containing $m$. Since more than $2f$ processes have proposed $m$, at least one of them must be correct and be elected as a winner. Therefore, there exist a round $r$ and a winner $j \in \winners[r]$ such that $m \in S_j$ was broadcast by $p_j$.
|
|
\end{proof}
|
|
|
|
\begin{lemma}[Eventual Closure]\label{lem:bft-eventual-closure}
|
|
For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
Let $p_i$ be a correct process such that $\unordered \setminus \ordered \neq \emptyset$ after round $r$ is the highest closed round it observed. By the main loop of Algorithm~\ref{alg:bft-arb}, $p_i$ eventually enters round $r+1$, computes $S=\unordered\setminus\ordered$, and invokes $\RBcast(\texttt{PROP},S,\langle i,r+1\rangle)$.
|
|
|
|
By RB Validity, every correct process eventually $\rdeliver(\texttt{PROP},S,\langle i,r+1\rangle)$. Upon this delivery, each correct process executes $\BFTPROVE(\langle i,r+1\rangle)$. Hence at least $n-t$ correct processes issue a proof for candidate $i$ in round $r+1$, and in particular the threshold $t+1$ used in $\validated(r+1)$ is eventually met for that candidate.
|
|
|
|
The same argument applies to each correct process that broadcasts in round $r+1$: once its proposal is RB-delivered, at least $n-t$ correct processes issue the corresponding proofs, so that sender is eventually included in $\validated(r+1)$. Since there are at least $n-t$ correct processes, eventually $|\validated(r+1)| \geq n-t$, and the wait at line~\ref{alg:check-validated} is eventually released for every correct process in that round.
|
|
|
|
After this point, each correct process executes the $\BFTAPPEND$ loop (line~\ref{alg:append}) and sends $\texttt{DONE}$ to all processes. By reliability of point-to-point channels, every correct process eventually receives at least $n-t$ DONE messages, so the wait at line~\ref{alg:check-done} is also eventually released. At that moment, the process computes $\winners[r+1] \gets \validated(r+1)$, and by the previous bound we have $|\winners[r+1]| \geq n-t$.
|
|
|
|
Therefore round $r+1$ eventually becomes closed with at least $n-t$ winners.
|
|
\end{proof}
|
|
|
|
\begin{lemma}[Total Order]\label{lem:bft-total-order}
|
|
For any two correct processes $p_i$ and $p_j$, the sequence $\ordered$ maintained locally by $p_i$ and the sequence maintained by $p_j$ contain the same messages in the same order, provided that both have reached the same set of closed rounds.
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
|
We prove the claim by induction on the number of closed rounds completed by both processes.
|
|
|
|
\textbf{Base case.} Before any closed round is completed, both local sequences are initialized to $\epsilon$, hence identical.
|
|
|
|
\textbf{Induction step.} Assume that after all closed rounds up to $r-1$, processes $p_i$ and $p_j$ have identical $\ordered$ prefixes. Consider round $r$.
|
|
|
|
By \Cref{lem:winners-stability}, once round $r$ is closed, both processes use the same stable winner set $\winners[r]$. By \Cref{lem:message-content-invariance}, the set $M$ computed at line~\ref{code:Mcompute} is identical at all correct processes for that round. Both processes then apply the same deterministic ordering function $\order(M)$ and append that same ordered block to their current sequence.
|
|
|
|
Since they started round $r$ from identical prefixes and append the same ordered suffix for round $r$, their resulting sequences after round $r$ are identical. The induction concludes that for any common set of closed rounds, both correct processes maintain the same messages in the same order.
|
|
\end{proof}
|
|
|
|
\begin{theorem}
|
|
The algorithm implements a BFT Atomic Reliable Broadcast.
|
|
\end{theorem}
|