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

\paragraph{Termination.} Every operation $\APPEND(x)$, $\PROVE(x)$, and $\READ()$ invoked by a correct process always returns.

\paragraph{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if:
\begin{itemize}
  \item $p \in \Pi_M \subseteq \Pi$; \textbf{and}
  \item $x \in S$, where $S$ is a predefined set.
\end{itemize}
Otherwise, the operation is invalid.

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

\paragraph{PROVE Anti-Flickering.} If the invocation of a operation $op = \PROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\PROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.

\paragraph{READ Validity.} The invocation of $op = \READ()$ by a process $p$ returns the list of valid invocations of $\PROVE$ 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{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{ABbroadcast$(m)$}
    \begin{algorithmic}[1]
        \State $r \gets \current$
        \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$}
            \State $\RBcast(i, PROP, m, 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 \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
    \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}
