
\subsection{Model extension}
We consider a static set of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable.

\paragraph{Synchrony.} The network is asynchronous. Processes may crash or be byzantine; at most $f = \frac{n}{2} - 1$ processes can be faulty.

\paragraph{Communication.} Processes can exchange through a Reliable Broadcast (\RB) primitive (defined below) which's invoked with the functions \RBcast$(m)$ and \RBreceived$(m)$. There exists a shared object called DenyList (\DL) (defined below) that is interfaced with the functions \APPEND$(x)$, \PROVE$(x)$ and \READ$()$.

\paragraph{Byzantine behaviour}
A process exhibits Byzantine behavior if it deviates arbitrarily from the specified algorithm. This includes, but is not limited to, the following actions:

\begin{itemize}
  \item Invoking primitives (\RBcast, \APPEND, \PROVE, etc.) with invalid or maliciously crafted inputs.
  \item Colluding with other Byzantine processes to manipulate the system's state or violate its guarantees.
  \item Delaying or accelerating message delivery to specific nodes to disrupt the expected timing of operations.
  \item Withholding messages or responses to create inconsistencies in the system's state.
\end{itemize}

Byzantine processes are constrained by the following:
\begin{itemize}
  \item They cannot forge valid cryptographic signatures or threshold shares without the corresponding private keys.
  \item They cannot violate the termination, validity, or anti-flickering properties of the \DL{} object.
  \item They cannot break the integrity, no-duplicates, or validity properties of the \RB{} primitive.
\end{itemize}

\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $M \subseteq \Pi$ (processes allowed to issue \APPEND) and $V \subseteq \Pi$ (processes allowed to issue \PROVE). Indices $i,j \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$ for the \DL{} linearization: $x \prec y$ means that operation $x$ appears strictly before $y$ in the linearized history of \DL. 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 round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.

% ------------------------------------------------------------------------------
\subsection{Primitives}

\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(x)$ such that : 

\paragraph{Termination.} Every operation $\BFTAPPEND(x)$, $\BFTPROVE(x)$, and $\BFTREAD()$ invoked by a correct process always returns.

\paragraph{APPEND Validity.} The invocation of $\BFTAPPEND(x)$ by a correct process $p_i$ is valid iff $i \in \Pi_M$. Otherwise the operation is invalid.

\paragraph{PROVE Validity.} If the invocation of a $op = \BFTPROVE(x)$ by a correct process $p$ is not valid, then:
\begin{itemize}
  \item $p \not\in \Pi_V$; \textbf{or}
  \item At least $t+1$ valid $\BFTAPPEND(x)$ appears before $op$ in $\Seq$.
\end{itemize}
Otherwise, the operation is valid.

\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 Validity.} The invocation of $op = \BFTREAD()$ by a process $p$ returns the list of valid invocations of $\BFTPROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation.

\subsubsection{t-BFT-GE}

We consider a t-Byzantine Fault Tolerant Group Election Object (t-$\BFTGE[r]$) per round $r \in \mathcal{R}$ with the following properties.

There are three operations: $\BFTVOTE(j, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$.

\paragraph{Termination.} Every operation $\BFTVOTE(i, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$ invoked by a correct process always returns.

\paragraph{Stability.} If there exist at least $n-f$ invocations of $\BFTCOMMIT(r)$ by distincts processes and let call $\BFTCOMMIT(r)^\star$ the $(n-f)^{th}$ such invocation in the linearization of $\Seq$. Then any invocation of $\BFTRESULT(r)$ that appears after $\BFTCOMMIT(r)^\star$ in $\Seq$ returns the same set of processes $W_r$.

\paragraph{VOTE-Validity.} The invocation of $\BFTVOTE(j, r)$ by a correct process is not valid if $\BFTCOMMIT(r)^\star$ appears before in $\Seq$. Otherwise, the operation is valid.

\paragraph{Election.} If at least $f+1$ correct processes invoked a valid $\BFTVOTE(j, r)$ for the same process $j$ then $j$ will be enventually included in the set $W_r$ returned by $\BFTRESULT(r)$. 

\subsection{DL $\Rightarrow$ t-BFT-DL}

\begin{lemma}
    For any fixed value $t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
\end{lemma}

\begin{proof}
    Fix $t < |M|$. Let
    \[
    \mathcal{T} \triangleq \{\, T \subseteq M \mid |T| = t \,\}.
    \]
    For each $T \in \mathcal{T}$, we instantiate one DenyList object $DL_T$ whose authorization sets are
    \[
    \Pi_M(DL_T) \triangleq S_T \triangleq M \setminus T
    \qquad\text{and}\qquad
    \Pi_V(DL_T) \triangleq V.
    \]
    Let
    \[
    K \triangleq \{\, DL_T \mid T \in \mathcal{T} \,\},
    \qquad\text{so that}\qquad
    |K| = \binom{|M|}{t}.
    \]


    % The system consists of a set of $\Pi$ processes, we define a subset of processes $M \subseteq \Pi$ which are authorized to invoke the $\BFTAPPEND$ operation and a subset of processes $V \subseteq \Pi$ which are authorized to invoke the $\BFTPROVE$ operation.
    
    % There exist $K$ a set of $\binom{|M|}{t+1}$ DenyList objects denoted by $DL_1, DL_2, \dots, DL_{|K|}$ such that each DenyList $DL_k$ is associated with a unique subset of processes $S_k \subseteq M$ of size $t+1$.
    
    \begin{algorithmic}
        \State $K \gets \{DL_1, DL_2, \dots, DL_{|K|}\}$ \Comment{Set of DenyList objects}
        \vspace{1em}
        \Function{BFTAPPEND}{x}
            \If{$p_i \not\in \Pi_M$}
                \State \Return \textbf{false}
            \EndIf
            \For{\textbf{each } $DL_k \in K$ \textbf{such that} $p_i \in S_k$}
                \State $DL_k.\APPEND(x)$
            \EndFor
            \State \Return \textbf{true}
        \EndFunction
        \vspace{1em}
        \Function{BFTPROVE}{x}
            \For{\textbf{each } $DL_k \in K$}
                \State $state \gets DL_k.\PROVE(x) || state$
            \EndFor
            \State \Return $state$
        \EndFunction
        \vspace{1em}
        \Function{BFTREAD}{}
            \State $results \gets \emptyset$
            \For{\textbf{each } $DL_k \in K$}
                \State $res \gets DL_k.\READ()$
                \State $results \gets results \cup res$
            \EndFor
            \State \Return $results$
        \EndFunction
        \vspace{1em}
    \end{algorithmic} 

    \textbf{APPEND Validity.} A process $p_i$ not in $\Pi_M$ who invokes $\BFTAPPEND(x)$ will never be able to submit a valid $\APPEND(x)$ to any DenyList $DL_k$ since each DenyList $DL_k$ is associated with a unique subset of processes $S_k \subseteq M$. Otherwise, if $p_i \in \Pi_M$, then any invocation of $\BFTAPPEND(x)$ are valid.
    
    \textbf{PROVE Validity.}
    Let set $op$ a particular invocation of $\BFTPROVE(x)$ by $p_i$.
    \begin{itemize}
        \item Case 1: If $p_i \not\in \Pi_V$, then $op$ is invalid since $p_i$ is not authorized to invoke $\PROVE$ operation in any DL.
        \item Case 2: If at least $t+1$ valid $\BFTAPPEND(x)$ submitted by $t+1$ distincts processus appears before $op$ in $\Seq$, then for any set $S_k$ there is at least one process in $S_k$ who submitted a valid $\APPEND(x)$ before $op$. Therefore, $op$ will be invalid since all $DLs$ will be locked on the value $x$ by the PROVE Validity of DL Object. 
    \end{itemize}
    Otherwise $op$ is always valid.

    \textbf{PROVE Anti-Flickering.}
    Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i \in \Pi_V$ that is \emph{invalid} in $\Seq$.
    By the \textbf{PROVE Validity} of t-$\BFTDL$, this implies that there exist at least $t+1$ \emph{valid}
    invocations of $\BFTAPPEND(x)$ by $t+1$ distinct processes that appear before $op$ in $\Seq$.
    Let $A \subseteq \Pi_M$ be the set of these (distinct) issuers, with $|A|\ge t+1$.
    
    Consider any DenyList object $DL_k \in K$, associated with a subset $S_k \subseteq M$ of size $|S_k|=t+1$.
    Since $K$ contains \emph{all} $(t+1)$-subsets of $M$ and $|A|\ge t+1$, we have
    \[
    S_k \cap A \neq \emptyset.
    \]
    Let $p_j \in S_k \cap A$. By construction of $\BFTAPPEND$, the invocation $\BFTAPPEND^{(j)}(x)$ triggers
    the operation $DL_k.\APPEND(x)$ (because $p_j \in S_k$), and since $\BFTAPPEND^{(j)}(x) \prec op$ in $\Seq$,
    this $DL_k.\APPEND(x)$ appears before the operation $DL_k.\PROVE(x)$ induced by $op$ in the linearization $\Seq_k$
    of $DL_k$.
    
    Therefore, in $\Seq_k$ there exists a valid $\APPEND(x)$ before the invocation $DL_k.\PROVE(x)$ induced by $op$.
    By the \textbf{PROVE Validity} property of $\DL$, this implies that the invocation $DL_k.\PROVE(x)$ induced by $op$
    is \emph{invalid}. Since this holds for every $k \in K$, all component $\PROVE$ operations of $op$ are invalid.
    
    Now consider any invocation $op'=\BFTPROVE(x)$ that appears after $op$ in $\Seq$.
    For each $k$, the invocation of $DL_k.\PROVE(x)$ induced by $op'$ appears after the one induced by $op$ in $\Seq_k$.
    By the \textbf{PROVE Anti-Flickering} property of $\DL$, once a $\PROVE(x)$ is invalid in $\Seq_k$,
    all subsequent $\PROVE(x)$ in $\Seq_k$ are invalid. Hence, for all $k$, the $\PROVE(x)$ induced by $op'$ is invalid,
    which implies that $op'$ is invalid at the t-$\BFTDL$ level.
    This proves the \textbf{PROVE Anti-Flickering} property for the construction.
    
    \medskip
    \textbf{READ Validity.}
    Let $op=\BFTREAD()$ be an invocation by a correct process $p$.
    The algorithm executes, for each $DL_k \in K$, a read $res_k \gets DL_k.\READ()$ and returns
    \[
    results \;=\; \bigcup_{k\in K} res_k.
    \]
    By \textbf{READ Validity} of each $\DL$, $res_k$ contains exactly the valid invocations of $\PROVE$
    that appear before $DL_k.\READ()$ in $\Seq_k$, together with the identities of their issuers.
    
    We show that $results$ is exactly the set of valid invocations of $\BFTPROVE$ that appear before $op$ in $\Seq$.
    
    \smallskip
    \emph{(i) Soundness (no false positives).}
    Take any entry $(j,\PROVE(x)) \in results$. Then $(j,\PROVE(x)) \in res_k$ for some $k$,
    hence the invocation $DL_k.\PROVE(x)$ by $p_j$ is valid and appears before $DL_k.\READ()$ in $\Seq_k$.
    In particular, there is no valid $DL_k.\APPEND(x)$ before that $DL_k.\PROVE(x)$ in $\Seq_k$
    (otherwise $DL_k.\PROVE(x)$ would be invalid by \textbf{PROVE Validity} of $\DL$).
    
    Assume by contradiction that the corresponding invocation $\BFTPROVE^{(j)}(x)$ is invalid in $\Seq$.
    Then, by \textbf{PROVE Validity} of t-$\BFTDL$, there exist at least $t+1$ valid invocations of $\BFTAPPEND(x)$
    by $t+1$ distinct processes before $\BFTPROVE^{(j)}(x)$ in $\Seq$.
    As in the argument used for \textbf{PROVE Anti-Flickering}, this implies that for every $DL_{k'} \in K$,
    there exists a valid $DL_{k'}.\APPEND(x)$ before the $DL_{k'}.\PROVE(x)$ induced by $\BFTPROVE^{(j)}(x)$.
    Therefore the induced $DL_k.\PROVE(x)$ would be invalid, contradicting $(j,\PROVE(x)) \in res_k$.
    Hence $\BFTPROVE^{(j)}(x)$ is valid and appears before $op$ in $\Seq$.
    
    \smallskip
    \emph{(ii) Completeness (no omissions).}
    Consider a valid invocation $\BFTPROVE^{(j)}(x)$ that appears before $op=\BFTREAD()$ in $\Seq$.
    Let $A$ be the set of distinct processes that invoked a valid $\BFTAPPEND(x)$ before $\BFTPROVE^{(j)}(x)$ in $\Seq$.
    Since $\BFTPROVE^{(j)}(x)$ is valid in t-$\BFTDL$, we have $|A| \le t$.
    
    Because $K$ contains all subsets $S_k \subseteq M$ of size $t+1$ and $t<|M|$,
    there exists some $S_k$ such that
    \[
    S_k \cap A = \emptyset.
    \]
    For this $DL_k$, none of the $\BFTAPPEND(x)$ invocations issued by processes in $A$
    triggers $DL_k.\APPEND(x)$ (since $\BFTAPPEND$ calls $DL_k.\APPEND(x)$ only for $k$ with issuer in $S_k$).
    Thus, there is no valid $DL_k.\APPEND(x)$ before the invocation $DL_k.\PROVE(x)$ induced by $\BFTPROVE^{(j)}(x)$.
    By \textbf{PROVE Validity} of $\DL$, the induced $DL_k.\PROVE(x)$ is valid.
    Moreover, since $\BFTPROVE^{(j)}(x) \prec \BFTREAD()$ in $\Seq$, this induced $\PROVE(x)$ appears before
    $DL_k.\READ()$ in $\Seq_k$, and therefore it is included in $res_k$.
    Hence $(j,\PROVE(x)) \in results$.
    
    Combining (i) and (ii), $results$ contains exactly the valid invocations of $\BFTPROVE$
    that appear before $op$ in $\Seq$, together with the identities of their issuers.
    This proves the \textbf{READ Validity} property.
    
\end{proof}


\subsection{t-BFT-DL $\Rightarrow$ t-BFT-GE}

\begin{lemma}
    For any fixed value $r \in S$, multiple BFT-DenyList Object can be used to implement a BFT-Group Election Object.
\end{lemma}

\begin{proof}
    \begin{algorithmic}
        \State $Y[i]$ \Comment{Is a set of $n$ $\BFTDL$ with $\Pi_M = \Pi_V = \Pi$}

        \vspace{1em}

        \Function{BFTVOTE}{j, r}

        \EndFunction
        \vspace{1em}

        \Function{BFTCOMMIT}{r}
        \EndFunction
        \vspace{1em}
        \Function{BFTRESULT}{r}
            \State $Z \gets \emptyset$
            \For{\textbf{each } $j \in \Pi$}
                \If{$|\{(\_, \PROVEtrace(\_, r)) \in Y[j].\BFTREAD(r)\}| \geq n-f$}
                    \State $P \gets \BFTREAD()$
                    \State \Return $\{j : (j, \PROVEtrace), \}$
                \EndIf
            \EndFor
        \EndFunction
        \vspace{1em}
    \end{algorithmic}
\end{proof}

\subsection{Algorithm}

\subsubsection{Variables}
Each process $p_i$ maintains the following local variables:
\begin{algorithmic}
  \State $\current \gets 0$
  \State $\received \gets \emptyset$
  \State $\delivered \gets \emptyset$
  \State $\prop[r][j] \gets \bot, \forall r, j$
%   \State $X_r \gets \bot, \forall r$
  \State $W_r \gets \bot, \forall r$
  \State $\resolved[r] \gets \bot, \forall r$
\end{algorithmic}

\renewcommand{\algletter}{A}
\begin{algorithm}[H]
    \caption{ABroadcast$(m)$}
    \begin{algorithmic}[1]
        \Function{ABroadcast}{$m$}
            \State $r \gets \current$
            \State $S \gets (\received \cup \{m\}$)
            \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$}
                \State $\RBcast(i, PROP, S, r)$
                \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \BFTRESULT[r]$
                \State $\BFTCOMMIT(r)$
                \State \textbf{wait} until $|\resolved[r]| \geq n - f$
                \State $W_r \gets \BFTRESULT[r]$
                \If{$i \in W_r \vee (\exists j, r': j \in W_r \wedge \prop[r'][j] \ni m)$}
                    \State \textbf{break}
                \EndIf
            \EndFor
        \EndFunction
    \end{algorithmic}
\end{algorithm}

\renewcommand{\algletter}{B}
\begin{algorithm}[H]
    \caption{ADeliver$(m)$}
    \begin{algorithmic}[1]
        \Function{ADeliver}{m}
            \State $r \gets \current$
            \If{$|\resolved[r]| < n - f$}
                \State \Return $\bot$
            \EndIf
            \State $W_r \gets \BFTRESULT[r]$
            \If{$\exists j \in W_r,\ \prop[r][j] = \bot$} 
                \State \Return $\bot$
            \EndIf
            \State $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$
            \State $m \gets \ordered(M_r \setminus \delivered)[0]$ \Comment{Set $m$ as the smaller message not already delivered}
            \State $\delivered \leftarrow \delivered \cup \{m\}$
            \If{$M_r \setminus \delivered = \emptyset$} \Comment{Check if all messages from round $r$ have been delivered}
                \State $\current \leftarrow \current + 1$
            \EndIf
            \State \textbf{return} $m$
        \EndFunction
    \end{algorithmic}
\end{algorithm}

\renewcommand{\algletter}{C}
\begin{algorithm}[H]
    \caption{RB handlers}
    \begin{algorithmic}[1]
        \Function{Rreceived}{j, PROP, S, r}
            \State $\received \gets \received \cup \{S\}$
            \State $\prop[r][j] \gets S$
            \State $\BFTVOTE(j, r)$
        \EndFunction

        \vspace{1em}
        
        \Function{Rreceived}{j, COMMIT, r}
            \State $\received[r] \cup \{j\}$
        \EndFunction
    \end{algorithmic}
\end{algorithm}

% \subsection{Example execution}

% \begin{figure}[H]
%   \centering
%   \input{diagrams/classic_seq.tex}
%   \caption{Expected Executions of P1 willing to send a message at round r}
% \end{figure}
