reorganisation + propriétés de TRNG

Recherche/BFT-ARBover/main.tex

@@ -59,10 +59,17 @@
 \newcommand{\Messages}{\mathsf{Messages}}
 \newcommand{\ABlisten}{\textsf{AB-listen}}
 
+\newcommand{\CANDIDATE}{\mathsf{CANDIDATE}}
+\newcommand{\CLOSE}{\mathsf{CLOSE}}
+\newcommand{\READGE}{\mathsf{READGE}}
+
 \newcommand{\SHARE}{\mathsf{SHARE}}
 \newcommand{\COMBINE}{\mathsf{COMBINE}}
 \newcommand{\VERIFY}{\mathsf{VERIFY}}
 
+\newcommand{\RETRIEVE}{\mathsf{RETRIEVE}}
+\newcommand{\SUBMIT}{\mathsf{SUBMIT}}
+
 \newcommand{\delivered}{\mathsf{delivered}}
 \newcommand{\received}{\mathsf{received}}
 \newcommand{\prop}{\mathsf{prop}}
@@ -70,6 +77,7 @@
 \newcommand{\current}{\mathsf{current}}
 
 \newcommand{\Seq}{\mathsf{Seq}}
+\newcommand{\GE}{\mathsf{GE}}
 
 \crefname{theorem}{Theorem}{Theorems}
 \crefname{lemma}{Lemma}{Lemmas}
@@ -100,11 +108,29 @@ We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$
   \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
 \end{itemize}
 
-\subsection{DenyList (DL)}
+\subsection{Group Election Object}
-We assume a synchronous DenyList (\DL) object with the following properties.
 
-The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
+We consider a Groupe Election object ($\GE[r]$) per round $r \in \mathcal{R}$ with the following properties.
+
+There are three operations: $\CANDIDATE(r), \CLOSE(r)$ and $\READGE(r)$ such that:
 \begin{itemize}
+  \item \textbf{Termination.} A $\CANDIDATE(r), \CLOSE(r)$ or $\READGE(r)$ operation invoked by a correct process always returns.
+  \item \textbf{Election.} If there exists at least one $\CLOSE(r)$ operation and let $\CLOSE(r)^\star$ denote the first $\CLOSE(r)$ in the linearization order. If some correct process $p$ invokes $\CANDIDATE(r)$ and the invocation of $\CANDIDATE(r)$ appears before $\CLOSE(r)^\star$ in the linearization order, then $\Winners_r \neq \emptyset$.
+  \item \textbf{Prefix Inclusion.} If $\CLOSE(r)^\star$ exists, then there exists a set $\Winners_r \subseteq \Pi$ such that, for any process $p_j$: $p_j \in \Winners_r$ iff $p_j$ invokes $\CANDIDATE(r)$ and its $\CANDIDATE(r)$ operation is linearized before $\CLOSE(r)^\star$.
+  \item \textbf{Stability.} If $\CLOSE(r)^\star$ exists, then every $\READGE(r)$ operation linearized after
+  $\CLOSE(r)^\star$ returns exactly $\Winners_r$.
+  \item \textbf{READ Validity.} The invocation of $op = \READGE(r)$ by a process $p$ returns the list of valid invocations of $\CANDIDATE(r)$ that appears before $op$ in the linearization order along with the names of the processes that invoked each operation.
+\end{itemize}
+
+
+
+\section{Group Election Object Consensus Number}
+
+\begin{definition}
+  We assume a synchronous DenyList (\DL) object as in~\cite{frey:disc23} with the following properties.
+
+  The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
+  \begin{itemize}
     \item \textbf{Termination.} A $\PROVE$, an $\APPEND$, or a $\READ$ operation invoked by a correct process always returns.
     \item \textbf{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if:
     \begin{itemize}
@@ -120,8 +146,116 @@ The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\R
     Otherwise, the operation is valid.
     \item \textbf{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.
     \item \textbf{READ Validity.} The invocation of $op = \READ()$ by a process $p \in \pi_V$ 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. 
-  \item \textbf{Anonymity.} Let us assume the process $p$ invokes a $\PROVE(v)$ operation. If the process $p'$ invokes a $\READ()$ operation, then $p'$ cannot learn the value $v$ unless $p$ leaks additional information.
+    item \textbf{Anonymity.} Let us assume the process $p$ invokes a $\PROVE(v)$ operation. If the process $p'$ invokes a $\READ()$ operation, then $p'$ cannot learn the value $v$ unless $p$ leaks additional information.
-\end{itemize}
+  \end{itemize}
+
+  We assume that $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).
+\end{definition}
+
+\begin{lemma}[From DenyList to Group Election]\label{lem:dl-to-ge}
+  For any fixed value $r \in S$, one DenyList object can be used to wait-free implement a Group Election object $\GE[r]$.
+\end{lemma}
+
+\begin{proof}
+  We implement the operations of $\GE[r]$ using the operations of the
+  DenyList as follows.
+  
+  \begin{algorithmic}
+    \Function{CANDIDATE}{$r$}
+      \State $\PROVE(r)$
+    \EndFunction
+    \vspace{1em}
+    \Function{CLOSE}{$r$}
+      \State $\APPEND(r)$
+    \EndFunction
+    \vspace{1em}
+    \Function{READGE}{$r$}
+      \State $P \gets \READ()$
+      \State \Return $\{ j : (j,\PROVEtrace(r)) \in P \}$
+    \EndFunction
+  \end{algorithmic}
+  
+  \paragraph{Termination.} Termination follows from the Termination property of DenyList operations. Consider now a fixed sequential history $\mathsf{Seq}$ of the DenyList.
+  \paragraph{Prefix Inclusion.} Let $\APPEND(r)^\star$ denote the first valid $\APPEND(r)$ in $\mathsf{Seq}$, if it exists. From the PROVE Validity and anti-flickering properties of the DenyList, a process $p_j$ has a valid $\PROVE(r)$ in $\mathsf{Seq}$ if and only if its $\PROVE(r)$ invocation appears before $\APPEND(r)^\star$ in $\mathsf{Seq}$.
+  Hence, by construction, $p_j \in \Winners_r$ iff $p_j$ invokes $\CANDIDATE(r)$ and its $\CANDIDATE(r)$ is linearized before $\CLOSE(r)^\star$ where we identify $\CLOSE(r)^\star$ with $\APPEND(r)^\star$. This is exactly the Prefix inclusion property.
+  \paragraph{Stability.} Moreover, after $\APPEND(r)^\star$, no new $\PROVE(r)$ can become valid (anti-flickering), so every subsequent $\READ^\star()$
+  returns the same set of valid $\PROVE(r)$ invocations. Consequently,
+  every $\READGE(r)$ linearized after $\CLOSE(r)^\star$ returns the same
+  set $\Winners_r$, which proves Stability.
+  \paragraph{Election.} Finally, if some process invokes $\CANDIDATE(r)$ before $\CLOSE(r)^\star$, its proof is valid and thus appears in the set returned by $\READ^\star()$. Hence $\Winners_r \neq \emptyset$, which proves Election.
+  \paragraph{Validity.} Validity is immediate from the construction of $\Winners_r$: a process belongs to $\Winners_r$ only if it invoked $\PROVE(r)$, i.e., only if it invoked $\CANDIDATE(r)$.
+
+  Thus the constructed object satisfies all properties of a Group Election object.
+\end{proof}
+
+\begin{lemma}[From Group Election to DenyList]\label{lem:ge-to-dl}
+  Fix a value $r \in S$. A Group Election object $\GE[r]$ can be used to wait-free implement an DenyList.
+\end{lemma}
+  
+\begin{proof}
+  We implement the  DenyList for value $r$ as follows.
+  We use one Group Election object $\GE[r]$.
+  
+  The operations are implemented as follows.
+    
+  \begin{algorithmic}
+    \Function{APPEND}{$r$}
+      \State $\CLOSE(r)$
+    \EndFunction
+    \vspace{1em}
+    \Function{PROVE}{$r$}
+      \State $\CANDIDATE(r)$
+      \State $W_r \gets \READGE(r)$
+      \If{$p \in W_r$}
+        \State \Return \texttt{True}
+      \Else
+        \State \Return \texttt{False}
+      \EndIf
+    \EndFunction
+    \vspace{1em}
+    \Function{READ}{$ $}
+      \State $W \gets \bigcup_{\forall r \in S}\READGE(r)$
+      \State \Return $\{(p,r) \mid p \in W_r\}$
+    \EndFunction
+  \end{algorithmic}
+
+  \paragraph{Termination.} Termination follows from the Termination property of Group Election operations. Consider now a fixed sequential history $\mathsf{Seq}$ of the Group Election.
+
+  \paragraph{APPEND Validity.} By construction, any process invoking $\APPEND(r)$ invokes $\CLOSE(r)$. By definition of Group Election, $\CLOSE(r)$ is always valid.
+
+  \paragraph{PROVE Validity.} By definition $\Pi_V = \Pi$, so any process invoking $\PROVE(r)$ is in $\Pi_V$. So the case $p \not\in \Pi_V$ cannot happen. Now, if some process invokes $\APPEND(r)$ before the invocation of $\PROVE(r)$ in $\mathsf{Seq}$, then by the Prefix Inclusion property of Group Election, the set $\Winners_r$ is already fixed and any subsequent $\CANDIDATE(r)$ cannot be in $\Winners_r$. Hence the invocation of $\PROVE(r)$ is invalid. Conversely, if no $\APPEND(r)$ appears before $\PROVE(r)$ in $\mathsf{Seq}$, then by the Election property of Group Election, if some correct process invoked $\CANDIDATE(r)$ before any $\CLOSE(r)$, then $\Winners_r \neq \emptyset$ and hence the invoking process belongs to $\Winners_r$. Thus its invocation of $\PROVE(r)$ is valid. This proves PROVE Validity.
+
+  \paragraph{PROVE Anti-Flickering.} If some invocation of $\PROVE(r)$ is invalid, then some $\APPEND(r)$ must have appeared before it in $\mathsf{Seq}$. By the Prefix Inclusion property of Group Election, the set $\Winners_r$ is fixed after the first $\CLOSE(r)$, so any subsequent $\CANDIDATE(r)$ cannot be in $\Winners_r$. Hence any subsequent invocation of $\PROVE(r)$ is also invalid. This proves PROVE Anti-Flickering.
+
+  \paragraph{READ Validity.} Finally, by construction, the invocation of $\READ()$ returns the list of valid invocations of $\PROVE$ that appear before it in $\mathsf{Seq}$ along with the names of the processes that invoked each operation. This proves READ Validity.
+
+\end{proof}  
+
+\begin{theorem}[Consensus number of Group Election]\label{thm:ge-consensus}
+  Let $|\Pi_V| = k$. The Group Election object type with verifier set $\Pi_V$
+  has consensus number $k$. In particular, when $\Pi_V = \Pi$, the consensus
+  number of Group Election is $|\Pi|$.
+\end{theorem}
+
+\begin{proof}
+  We first recall that, for a DenyList object with $|\Pi_V| = k$ (a
+  $k$-DenyList), the consensus number is exactly $k$.
+
+  \paragraph{Lower bound.}
+  By Lemma~\ref{lem:dl-to-ge}, for any fixed value $r \in S$, one $k$-DenyList object can be used to wait-free implement a Group Election object $\GE[r]$ over the same set of processes. Since the k-DenyList has consensus number $k$, it follows that the Group Election type has consensus number at least $k$.
+
+  \paragraph{Upper bound.}
+  Conversely, by Lemma~\ref{lem:ge-to-dl}, one Group Election object 
+  can be used to wait-free implement a DenyList object restricted to value $r$.
+  This restricted DenyList satisfies the same specification as the original k-DenyList on value $r$, and in particular it has consensus number $k$. Therefore, the consensus
+  number of the Group Election type cannot exceed $k$.
+
+  \medskip
+  Combining the two bounds, we obtain that the consensus number of the Group
+  Election object type is exactly $k = |\Pi_V|$. When we instantiate
+  $\Pi_V = \Pi$, we get that the consensus number of Group Election is $|\Pi|$.
+\end{proof}
+
 
 % ------------------------------------------------------------------------------
 \section{Target Abstraction: Atomic Reliable Broadcast (ARB)}
@@ -134,8 +268,204 @@ plus Integrity/No-duplicates/Validity (inherited from \RB and the construction).
 
 \section{ARB over RB and DL}
 
+In this part we're using the consensus number of the GE Object to show that it's possible to implement F-ARB with RB and our defined object. Also we present an algorithm which achieve this in section 7. 
+
+\begin{theorem}[RB + Group Election implements F-ARB]\label{thm:ge-to-farb}
+  In an asynchronous message-passing system with crash failure. We can wait-free implement a FIFO-Atomic Reliable Broadcast from a Reliable Broadcast (RB) primitive and one Group Election object $\GE[r]$ per round $r \in \mathbb{N}$.
+\end{theorem}
+
+\begin{proof}
+  By Theorem~\ref{thm:ge-consensus}, the Group Election object type with verifier set $\Pi_V$ has consensus number $|\Pi_V|$. In particular, when $\Pi_V = \Pi$, using one instance $\GE[r]$ per round $r$ we can implement wait-free consensus among all processes in~$\Pi$.
+
+  It is well known that, in a crash-prone asynchronous message-passing system, consensus and atomic (total order) broadcast are equivalent (defago et al): given consensus, one can implement atomic broadcast by using an infinite sequence of consensus instances to decide the sequence of messages to deliver, and conversely atomic broadcast can be used to implement consensus by deciding a single value in the first
+  position of the total order.
+
+  In our setting, we already have a Reliable Broadcast (RB) primitive, which provides RB-Validity, RB-Agreement, and RB-Integrity for the dissemination of messages. Using the consensus power provided by the Group Election objects, we can therefore apply the standard reduction from consensus to atomic broadcast: each position (or \emph{slot}) in the global delivery sequence is chosen by a consensus instance, whose proposals are messages that have been RB-delivered but not yet ordered. This yields an atomic
+  reliable broadcast (ARB) primitive.
+
+  To obtain FIFO-Atomic Reliable Broadcast (F-ARB), it suffices to enforce per-sender FIFO order on top of ARB. This can be done in the usual way by tagging each message broadcast by a process $p_i$ with a local sequence number $s \in \mathbb{N}$, and by ensuring that only the message with the smallest pending sequence number for $p_i$ is ever proposed to a consensus instance. As a result, for every sender $p_i$, messages with tags $(p_i,s)$ and $(p_i,t)$ with $s < t$ are decided (and thus delivered) in this order at all processes.
+
+  Hence, RB plus Group Election objects is sufficient to implement FIFO-Atomic Reliable Broadcast.
+\end{proof}
+
+
 % ------------------------------------------------------------------------------
 
+\section{BFT-ARB over RB and DL}
+
+
+\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{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}
+
+\section{Example of implementation of ARB with DL and RB}
+
+We present below an example of implementation of Atomic Reliable Broadcast (\ARB) using a Reliable Broadcast (\RB) primitive and a DenyList (\DL) object according to the model and notations defined in Section 2.
+
 \subsection{Algorithm}
 % granularité diff commentaire de code et paragraphe pre algo
 
@@ -626,175 +956,6 @@ Which are cover by our FIFO-\ARB specification.
   \caption{Example execution of the ARB algorithm with a byzantine process}
 \end{figure}
 
-\section{BFT-ARB over RB and DL}
-
-
-\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{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}
-
-\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. The function is defined as follows:
-
-\begin{itemize}
-  \item \textbf{$t$-reconstruction.} Given any subset $S$ of at least $t$ valid shares derived from the same value $r$, there exists a unique value $\sigma$ consistent with all shares in~$S$, and $\sigma$ can be efficiently reconstructed from~$S$.
-  \item \textbf{$(t-1)$-non-reconstructibility.} Given any subset $S$ of at most $t-1$ valid shares derived from the same value $r$, there exist two distinct values $\sigma$ and $\sigma'$ that are both consistent with all shares in~$S$. In particular, no algorithm that only sees the shares in $S$ can always distinguish whether the underlying value is $\sigma$ or $\sigma'$.  \item \textbf{Per-process non-equivocation.} For any process $p$ and value $r$, there is at most one valid share that $p$ can derive from $r$. Formally, if $\sigma$ and $\sigma'$ are two valid shares output by process $p$ from the same value $r$, then $\sigma = \sigma'$. In particular, a single process cannot emit two different valid shares for the same underlying value~$r$.
-\end{itemize}
-
-\paragraph{Interface.}
-For algorithmic purposes, we model the $t$-out-of-$n$ threshold random number generator
-as providing the following interface to each process $p \in \Pi$.
-
-\begin{itemize}
-  \item{$\mathsf{SHARE}_{p_i}(r)$:} On input a value $r$, run locally by process $p_i$, returns a valid share $\sigma_r^i$. By per-process share uniqueness, for any fixed $p_i$ and $r$ the value $\sigma_r^i$ is uniquely determined.
-
-  \item{$\mathsf{COMBINE}(S)$:} On a set $S$ of at least $t$ pairs $(p_i,\sigma_r^i)$, returns the reconstructed value $\sigma_r$. By $t$-reconstruction, this value is well defined and independent of the particular set $S$ of valid shares of size at least $t$.
-
-  \item{$\mathsf{VERIFY}(r,\sigma_{r'})$:} On input a value $r$ and a candidate value $\sigma_{r'}$, returns \textsf{true} if and only if there exists a set $S$ of at least $t$ valid shares for $r$ such that $\mathsf{Combine}(r,S) = \sigma_{r'}$, and \textsf{false} otherwise. We say that $\sigma_{r'}$ is \emph{valid for $r$} if $\mathsf{Verify}(r,\sigma_{r'})=\textsf{true}$.
-\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}
 
 \section{Implementation of BFT-DenyList and Threshold Cryptography}