
\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{BFT DenyList}
% We consider a \DL object that satisfies the following properties despite the presence of up to $f$ byzantine processes:
% \begin{itemize}
%   \item \textbf{Termination.} Every operation $\APPEND(x)$, $\PROVE(x)$, and $\READ()$ invoked by a correct process eventually returns.
%   \item \textbf{APPEND/PROVE/READ Validity.} The preconditions for invoking $\APPEND(x)$, $\PROVE(x)$, and $\READ()$ are respected (cf. \#2.2). The return values of these operations conform to the sequential specification of the \DL object.
%   \item \textbf{APPEND Justification.} For any element $x$, if an operation $\APPEND(x)$ invoked by a correct process completes successfully, then there exists at least one valid $\PROVE(x)$ operation that that precedes this $\APPEND(x)$ in the \DL linearization.
%   \item \textbf{PROVE Anti-Flickering.} Once an element $x$ has been appended to the \DL by any process, all subsequent invocations of $\PROVE(x)$ by any process return ``invalid''.
% \end{itemize}

% \subsection{BFT-GE}

% We consider a Group Election object ($\GE[r]$) per round $r \in \mathcal{R}$ with the following properties.

% There are three operations: $\CANDIDATE(r), \CLOSE(r), \READGE()$ such that :

% \begin{itemize}
%   \item \textbf{Termination} 
% \end{itemize}

\subsubsection{t-out-of-n Threshold Random Number Generator}

We consider a function that with t out of n shares any process can reconstruct a deterministic random number $s$ from a given $t$. There are two operations $\SUBMIT(r), \RETRIEVE(r)$ such that :

\begin{itemize}
  \item \textbf{Agreement.} For all $s_1, s_2$ returned by two distinct invokations $\RETRIEVE(r)$, if $s_1, s_2 \neq \bot$ then $s_1 = s_2$.
  \item \textbf{t-threshold.} If there exist a $s$ returned from an invokation of $\RETRIEVE(r)$. $s \neq \bot$ iff a set of process $X \subseteq \Pi$ such that $|X| \geq t$ invoke $\SUBMIT(r)$.
  \item \textbf{non-forgability.} It's computationally infeasibile for the adversary to compute a valid value $s$ frome a given $r$ if he corrupt $f < t$ process.
  \item \textbf{liveness.} If all correct processes invoke $\SUBMIT(r)$, then any correct process invoking $\RETRIEVE(r)$ eventually returns a value $s \neq \bot$.
  \item \textbf{injectivity.} For any two distinct rounds $r_1 \neq r_2$, the values $s_1, s_2$ returned by $\RETRIEVE(r_1)$ and $\RETRIEVE(r_2)$ respectively are distinct.
\end{itemize}


\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 $\resolved[r] \gets \bot, \forall r$
\end{algorithmic}

\renewcommand{\algletter}{D}
\begin{algorithm}[H]
  \caption{\ABbroadcast}\label{alg:ab-cast}
  \begin{algorithmic}[1]
    \Function{ABcast}{$m$}
    \State $S \gets (\received \setminus \delivered) \cup \{m\}$
    \State $\RBcast(prop, S, r, i)$
    \State \textbf{wait until} $|X_r| \geq f+1$
    \State $\sigma_r \gets \COMBINE(X_r)$
    \State $\PROVE(\sigma_r); \APPEND(\sigma_r);$
    \State $\RBcast(submit, S, \sigma_r, r, i)$
    \EndFunction
  \end{algorithmic}
\end{algorithm}

\renewcommand{\algletter}{E}
\begin{algorithm}[H]
  \caption{\ABdeliver}\label{alg:ab-deliver}
  \begin{algorithmic}[1]
    \Function{$\ABdeliver$}{}
      \State $r \gets \current; \sigma_r \gets \resolved[r];$
      \If{$\sigma_r == \bot$}
        \State \Return $\bot$
      \EndIf
      \State $P \gets \READ()$
      \If{$\forall j : (j,prove(\sigma_r)) \not\in P$}
        \State \Return $\bot$
      \EndIf
      \State $\APPEND(\sigma_r); P \gets \READ();$
      \State $W_r \gets \{j : (j, \PROVEtrace(\sigma_r)) \in P\}$
      \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)[0]$
      \State $\delivered \gets \delivered \cup \{m\};$
      \If{$M_r \setminus \delivered = \emptyset$}
        \State $\current \gets \current + 1;$
      \EndIf
      \State \Return $m$
    \EndFunction
  \end{algorithmic}

\end{algorithm}

\renewcommand{\algletter}{F}
\begin{algorithm}[H]
  \caption{RBreceived handler}\label{alg:rb-handler}
  \begin{algorithmic}[1]
    \Function{RBrcvd}{$prop, S_j, r_j, j$}
    \If{$r_j \geq r$}
    \State $\prop[r_j][j] = S_j$
    \State $\sigma^i_{r_j} \gets \SHARE(r_j)$
    \State $send_j(r, \sigma^i_{r_j})$
    \EndIf
    \EndFunction
  \end{algorithmic}
\end{algorithm}


\renewcommand{\algletter}{G}
\begin{algorithm}[H]
  \caption{RBreceived handler}\label{alg:rb-handler-2}
  \begin{algorithmic}[1]
    \Function{RBrcvd}{$submit, S_j, \sigma_{r_j}, r_j, j$}
      \If{$\VERIFY(r_j, \sigma_{r_j})$}
        \State $\resolved[r_j] \gets \sigma_{r_j}$
      \EndIf
    \EndFunction
  \end{algorithmic}
\end{algorithm}


\renewcommand{\algletter}{H}
\begin{algorithm}[H]
  \caption{Share received handler}\label{alg:share-handler}
  \begin{algorithmic}[1]
    \Function{received}{$r_j, \sigma^j_{r_j}, j$}
      \If{$r_j == r$}
        \State $X_r \gets X_r \cup \sigma^j_{r}$
      \EndIf
    \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}
