
\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.} 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 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.

\paragraph{Local consistency.} For all correct process $p_i$ such that $p_i$ invoke an valid $\BFTPROVE(x)$ before a $P \gets \BFTREAD()$ operation in his local execution. Then the set of valid $\BFTPROVE(x)$ in $P$ must contain the previous valid $\BFTPROVE(x)$.

\paragraph{Liveness} For all correct process $p_i$ such that $p_i$ invoke an invalid $\BFTPROVE(x)$ before a $P \gets \BFTREAD()$ operation in his local execution. Then the set of valid $\BFTPROVE(x)$ in $P$ must be the same for any $p_i$.

% \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$ such that $3t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
\end{lemma}

\begin{proof}
    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.
    \]
    Let
    \[
    K = \{\, DL_U \mid U \in \mathcal{U} \,\},
    \qquad\text{so that}\qquad
    |U| = \binom{|M|}{|M| - t}.
    \]

    \begin{algorithmic}[1]
        % \State $K \gets \{DL_T : T \subseteq M, |T|=t\}$

        \renewcommand{\algletter}{DL}
        \begin{algorithm}[H]
            \caption{\BFTAPPEND}
            \Function{$\BFTAPPEND$}{x}
                \For{\textbf{each } $DL_U \in K$ such that $p_i \in U$} 
                \State $DL_U.\APPEND(x)$
                \EndFor
            \EndFunction
        \end{algorithm}
        
        % \renewcommand{\algletter}{B}    
        \begin{algorithm}[H]
            \caption{\BFTPROVE}
            \Function{$\BFTPROVE$}{x}
                \State $state \gets false$
                \For{\textbf{each } $DL_U \in K$}
                    \State $state \gets state \textbf{ OR } DL_U.\PROVE(x)$
                \EndFor
                \State \Return $state$
            \EndFunction
        \end{algorithm}
        
        % \renewcommand{\algletter}{C}  
        \begin{algorithm}[H]
            \caption{\BFTREAD}
            \Function{$\BFTREAD$}{$\bot$}
                \State $results \gets \emptyset$
                \For{\textbf{each } $DL_U \in K$}
                    \State $results \gets results \cup DL_U.\READ()$
                \EndFor
                \State \Return $results$
            \EndFunction
        \end{algorithm}
    \end{algorithmic}
        
    % \paragraph{BFT-APPEND Validity.} Let $A\subseteq M$ be the set of distinct issuers that invoked a valid $\BFTAPPEND(x)$ Suppose by contradiction that there exists $T\in\mathcal{T}$ with $A\cap S_T=\emptyset$. Since $S_T=M\setminus T$, this implies $A\subseteq T$, hence $|A|\le |T|=t$, contradicting $|A|\ge t+1$.

    \paragraph{BFT-PROVE Validity.} 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 a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$.

    \begin{itemize}
        % \item \textbf{Case (i): $i\notin V$.}
        % For every $T\in\mathcal{T}$, we configured $\Pi_V(DL_T)=V$, hence the induced operation $DL_T.\PROVE(x)$ is invalid by \textbf{PROVE Validity} of $\DL$. Therefore $op$ is invalid.
        
        \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 \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $T\in\mathcal{T}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so $op$ is invalid.
        
        \item \textbf{Case (ii): $|A|\le t$.}
        Fix any $U\in\mathcal{U}$, 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 V=\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 by the lifting convention $op$ is valid.
    \end{itemize}
        
    \smallskip
    Combining the cases yields the claimed characterization of invalidity.

    \paragraph{BFT-PROVE Anti-Flickering.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i\in V$ 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$.

    Now 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.
    

    \paragraph{Local consistency.}
    
    \paragraph{Liveness.}

\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}
