ajout biblio

Recherche/ALDLoverAB/main.tex

@@ -225,7 +225,7 @@ Each process $p_i$ maintains:
 % ------------------------------------------------------------------------------
 \section{Correctness}
 
-\begin{lemma}[Stable round closure]\label{lem:closure-stable}
+\begin{lemma}[Stable round closure]\label{rem:closure-stable}
 If a round $r$ is closed, then there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid.
 Once closed, a round never becomes open again.
 \end{lemma}

Recherche/BFT-ARBover/2_Primitives/index.tex

@@ -0,0 +1,25 @@
+\subsection{DenyList Object}
+
+ We assume a linearizable DenyList (\DL) object, following the specification 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}
+        \item $p \in \Pi_M \subseteq \Pi$; \textbf{and}
+        \item $x \in S$, where $S$ denote the universe of valid entries to be appended to the DenyList.
+      \end{itemize} 
+      Otherwise, the operation is invalid.
+      \item \textbf{PROVE Validity.} Let $op$ the invocation of $\PROVE(x)$ by a process $p_i$. We said $op$ to be invalid, if and only if:  
+      \begin{itemize}
+        \item $p \not\in \Pi_V \subseteq \Pi$; \textbf{or}
+        \item A valid $\APPEND(x)$ appears before $op$ in $\Seq$. 
+      \end{itemize}
+      Otherwise, the operation is said to be 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.
+    \end{itemize}
+  
+    We assume that $\Pi_M = \Pi_V = \Pi$ (all processes can invoke $\APPEND$ and $\PROVE$).

Recherche/BFT-ARBover/3_ARB_Def/index.tex

@@ -0,0 +1,11 @@
+
+Processes export \ABbroadcast$(m)$ and $m = \ABdeliver()$. We adopt the standard Atomic Broadcast specification of~\cite{Defago2004}. \ARB requires the following properties:
+\begin{itemize}[leftmargin=*]
+  \item \textbf{Total Order}: 
+  \begin{equation*}
+    \forall m_1,m_2,\ \forall p_i,p_j:\ \ (m_1 = \ABdeliver_i()) \prec (m_2 = \ABdeliver_i()) \Rightarrow (m_1 = \ABdeliver_j()) \prec (m_2 = \ABdeliver_j())
+  \end{equation*}
+  \item \textbf{Integrity}: Every message delivered was previously broadcast. $\forall p_i:\ m = \ABdeliver_i() \Rightarrow \exists p_j:\ \ABbroadcast_j(m)$.
+  \item \textbf{No-duplicates}: No message is delivered more than once at any process.
+  \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually delivers $m$.
+\end{itemize}

Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex

@@ -0,0 +1,374 @@
+We present below an example of implementation of Atomic Reliable Broadcast (\ARB) using point-to-point reliable, error-free channels and a DenyList (\DL) object according to the model and notations defined in Section 2.
+
+\subsection{Algorithm}
+
+\begin{definition}[Closed round]\label{def:closed-round}
+  Given a \DL{} linearization $H$, a round $r\in\mathcal{R}$ is \emph{closed} in $H$ if $H$ contains an operation $\APPEND(r)$.
+  Equivalently, there exists a time after which every $\PROVE(r)$ is invalid in $H$.
+\end{definition}
+
+% \paragraph{DenyList.} The \DL is initialized empty. We assume $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).
+
+\subsubsection{Handlers and Procedures}
+
+\begin{algorithm}[H]
+  \caption{ARB at process $p_i$}\label{alg:arb-crash}
+  % \SetAlgoLined
+
+  \SetKwBlock{LocalVars}{Local Variables:}{}
+  \LocalVars{
+    $\unordered \gets \emptyset$,
+    $\ordered \gets \epsilon$,
+    $\delivered \gets \epsilon$\;
+    $\prop[r][j] \gets \bot,\ \forall r,j$\;
+  }
+
+  \vspace{0.3em}
+
+  \For{$r = 1, 2, \ldots$}{
+    \textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
+    $S \leftarrow (\unordered \setminus \ordered)$\;\nllabel{code:Sconstruction}
+    \lForEach{$j \in \Pi$}{
+      $\send(\texttt{PROP}, S, \langle r, i \rangle) \textbf{ to } p_j$
+    }
+    $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
+
+    $\winners[r] \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute}
+    
+    \textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$\;\nllabel{code:check-winners-ack}
+    
+    $M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute-dl}
+    $\ordered \leftarrow \ordered \cdot \order(M)$\;\nllabel{code:next-msg-extraction}
+  }
+
+  \vspace{0.3em}
+
+  \Upon{$\ABbroadcast(m)$}{
+    $\unordered \gets \unordered \cup \{m\}$\;\nllabel{code:abbroadcast-add}
+  }
+
+  \vspace{0.3em}
+
+  \Upon{$\receive(\texttt{PROP}, S, \langle r, j \rangle)$ from process $p_j$}{
+    $\unordered \leftarrow \unordered \cup \{S\}$\;\nllabel{code:receivedConstruction}
+    $\prop[r][j] \leftarrow S$\;\nllabel{code:prop-set}
+  }
+
+  \vspace{0.3em}
+
+  \Upon{$\ABdeliver()$}{
+    \lIf{$\ordered \setminus \delivered = \emptyset$}{
+      \Return{$\bot$}
+    }
+    let $m$ be the first element in $(\ordered \setminus \delivered$)\;\nllabel{code:adeliver-extract}
+    $\delivered \gets \delivered \cdot m$\;\nllabel{code:adeliver-mark}
+    \Return{$m$}
+  }
+
+\end{algorithm}
+
+\paragraph{Algorithm intuition.}
+The crash-tolerant algorithm is organized around round closure and winner extraction. By \Cref{def:closed-round,def:first-append,lem:closure-view,lem:winners}, once a round is closed, every correct process eventually reads the same winner set $\Winners_r$. By \Cref{lem:nonempty}, this set is never empty, and by \Cref{lem:winners-propose} every winner has necessarily sent its proposal to all processes before becoming a winner, exactly because sending precedes $\PROVE(r)$ and $\APPEND(r)$ at line~\ref{code:submit-proposition}. Under reliable channels, these winner proposals are eventually received by every correct process, so the waiting condition at line~\ref{code:check-winners-ack} eventually becomes true, which is formalized by \Cref{lem:eventual-closure}. Then, by \Cref{lem:convergence}, all correct processes compute the same set $M$ at line~\ref{code:Mcompute-dl}, and because line~\ref{code:next-msg-extraction} applies the same deterministic ordering function, they append messages in the same order; this is exactly the core mechanism later used in \Cref{lem:validity,lem:no-duplication,lem:total-order}.
+
+\subsection{Correctness}
+
+\begin{definition}[First APPEND]\label{def:first-append}
+  Given a \DL{} linearization $H$, for any closed round $r\in\mathcal{R}$, we denote by $\APPEND^{(\star)}(r)$ the earliest $\APPEND(r)$ in $H$.  
+\end{definition}
+
+\begin{remark}[Stable round closure]\label{rem:closure-stable}
+  If a round $r$ is closed, then there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid.
+  Once closed, a round never becomes open again.
+\end{remark}
+
+\begin{proof}
+  By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the linearization $H$. \\
+  $H$ is a total order of operations, the set of $\APPEND(r)$ operations is totally ordered, and hence there exists a smallest $\APPEND(r)$ in $H$. We denote this operation $\APPEND^{(\star)}(r)$ and $t_0$ its linearization point. \\
+  By the validity property of \DL, a $\PROVE(r)$ is valid iff $\PROVE(r) \prec \APPEND^{(\star)}(r)$. Thus, after $t_0$, no $\PROVE(r)$ can be valid. \\
+  $H$ is a immutable grow-only history, and hence once closed, a round never becomes open again. \\
+  Hence there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid and the closure is stable. 
+\end{proof}
+
+\begin{lemma}[Across rounds]\label{lem:across}
+  If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$, r' is also closed.
+\end{lemma}
+
+\begin{proof}
+  \emph{Base.} For a closed round $r=0$, the set $\{r' \in \mathcal{R} : r' < r\}$ is empty, so the claim holds.
+
+  \emph{Induction step.} Assume $r+1$ is closed. By \cref{def:first-append}, there exists an earliest operation $\APPEND^{(\star)}(r+1)$ in the \DL linearization $H$. Let $p_j$ be the process that invokes this operation.
+
+  In Algorithm~\ref{alg:arb-crash}, the call to $\APPEND(\cdot)$ appears at line~\ref{code:submit-proposition}, inside the loop indexed by rounds $1,2,\ldots$. Therefore, if $p_j$ reaches line~\ref{code:submit-proposition} for round $r+1$, then in the previous loop iteration (round $r$) process order implies that $p_j$ has already invoked $\APPEND(r)$ at the same line.
+
+  Hence an $\APPEND(r)$ exists in $H$, so round $r$ is closed by \cref{def:closed-round}. We proved:
+  \[
+    (r+1\ \text{closed}) \Rightarrow (r\ \text{closed}).
+  \]
+  By repeated application, if some round $r$ is closed, then every round $r' < r$ is also closed.
+\end{proof}
+
+\begin{definition}[Winner Invariant]\label{def:winner-invariant}
+  For any closed round $r$, define
+  \[
+    \Winners_r \triangleq \{ j : \PROVE_j(r) \prec \APPEND^\star(r) \}
+  \] 
+  called the unique set of winners of round $r$.
+\end{definition}
+
+\begin{lemma}[Invariant view of closure]\label{lem:closure-view}
+  For any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r)$ in their \DL view.
+\end{lemma}
+  
+\begin{proof}
+  Let's take a closed round $r$. By \Cref{def:first-append}, there exists $\APPEND^{(\star)}(r)$ the earliest $\APPEND(r)$ in the DL linearization.
+
+  Consider any correct process $p_i$ that invokes $\READ()$ after $\APPEND^\star(r)$ in the DL linearization. Since $\APPEND^\star(r)$ invalidates all subsequent $\PROVE(r)$, the set of valid tuples $(\_,r)$ retrieved by a $\READ()$ after $\APPEND^\star(r)$ is fixed and identical across all correct processes.
+
+  Therefore, for any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r )$ in their \DL view.
+\end{proof}
+
+\begin{lemma}[Well-defined winners]\label{lem:winners}
+  For any correct process $p_i$ and round $r$, if $p_i$ computes $\winners[r]$ at line~\ref{code:Wcompute}, then :
+  \begin{itemize}
+    \item $\Winners_r$ is defined;
+    \item the computed $\winners[r]$ is exactly $\Winners_r$.
+  \end{itemize}
+\end{lemma}
+
+\begin{proof}
+  Lets consider a correct process $p_i$ that reach line~\ref{code:Wcompute} to compute $\winners[r]$. \\
+  By program order, $p_i$ must have executed $\APPEND_i(r)$ at line~\ref{code:submit-proposition} before, which implies by \Cref{def:closed-round} that round $r$ is closed at that point. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\
+  By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:Wcompute} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\ \cdot ,r)$ such that
+  \[
+    \winners[r] = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
+  \]
+\end{proof}
+
+\begin{lemma}[Winners are non-empty]\label{lem:nonempty}
+  For any closed round $r$, there exists at least one process $p_j$ that invoked $\PROVE_j(r) \prec \APPEND^\star(r)$, so $\Winners_r \neq \emptyset$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Let $r$ be a closed round. By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the \DL linearization $H$. Let $p_i$ be the process invoking the earliest such operation, $\APPEND^{(\star)}(r)$.
+  
+  By program order in Algorithm~\ref{alg:arb-crash}, the call to $\APPEND(\cdot)$ at line~\ref{code:submit-proposition} is immediately preceded by $\PROVE(r)$. Thus $p_i$ must have invoked $\PROVE_i(r)$ before $\APPEND^{(\star)}(r)$, and by the sequence of code at line~\ref{code:submit-proposition}, this $\PROVE_i(r)$ executes before $\APPEND^{(\star)}(r)$ in the linearization.
+  
+  By \Cref{def:winner-invariant}, $p_i \in \Winners_r$. Hence $\Winners_r \neq \emptyset$.
+\end{proof}
+
+\begin{lemma}[Winners must propose]\label{lem:winners-propose}
+  For any closed round $r$, $\forall i \in \Winners_r$, process $p_i$ must have sent messages to all processes $j \in \Pi$, and hence any correct process $p_j$ will eventually receive $p_i$'s message for round $r$ and set $\prop[r][i]$ to a non-$\bot$ value.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exists a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order in Algorithm~\ref{alg:arb-crash}, $p_i$ must have sent messages to all $j \in \Pi$ at line~\ref{code:submit-proposition} before invoking $\PROVE(r)$.
+  
+  If $p_i$ is a correct process that completed sending to all processes, then by the reliable and error-free nature of the communication channels, every correct process $p_j$ will eventually receive $p_i$'s message, which sets $\prop[r][i] \leftarrow S$ at line~\ref{code:prop-set}. If $p_i$ crashes before sending to all processes, then $p_i$ cannot invoke a valid $\PROVE_i(r)$ afterwards, contradicting the assumption that $i \in \Winners_r$. Hence $p_i$ must have completed sending to all processes.
+\end{proof}
+
+\begin{definition}[Messages invariant]\label{def:messages-invariant}
+  For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r : prop^{(i)}[r][j] \neq \bot$, define
+  \[
+    \Messages_r \triangleq \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]
+  \]
+  as the set of messages proposed by the winners of round $r$.
+\end{definition}
+
+\begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
+  If a correct process $p_i$ define $M$ at line~\ref{code:Mcompute-dl}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. 
+\end{lemma}
+
+\begin{proof}[Proof]
+  Let take a correct process $p_i$ that computes $M$ at line~\ref{code:Mcompute-dl}. By \Cref{lem:winners}, $p_i$ computation is the winner set $\Winners_r$.
+
+  By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line~\ref{code:Mcompute-dl} where $p_i$ computes $M$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received messages from every winner $j \in \Winners_r$. By \Cref{lem:winners-propose}, each winner $j$ has sent messages to all processes including $p_i$. Thus, by the reliable and error-free nature of the channels, if $p_i$ is correct, it will eventually receive $j$'s message, setting $\prop^{(i)}[r][j] \neq \bot$ at line~\ref{code:prop-set}. Hence, $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$.
+\end{proof}
+
+\begin{lemma}[Unique proposal per sender per round]\label{lem:unique-proposal}
+  For any round $r$ and any process $p_i$, $p_i$ sends messages to all processes at most once for each round.
+\end{lemma}
+
+\begin{proof}[Proof]
+  In Algorithm~\ref{alg:arb-crash}, the only place where a process $p_i$ can send messages to all processes is at line~\ref{code:submit-proposition}, which appears inside the main loop indexed by rounds $r = 1, 2, \ldots$.
+  
+  Each iteration of this loop processes exactly one round value $r$, and within that iteration, messages are sent at most once (before the $\PROVE(r)$ and $\APPEND(r)$ calls). Since the loop variable $r$ takes each value $1, 2, \ldots$ at most once during the execution, process $p_i$ sends messages at most once for any given round $r$.
+\end{proof}
+
+\begin{lemma}[Proposal convergence]\label{lem:convergence}
+  For any round $r$, for any correct processes $p_i$ that execute line~\ref{code:Mcompute-dl}, we have
+  \[
+    M^{(i)} = \Messages_r
+  \]
+\end{lemma}
+
+\begin{proof}[Proof]
+  Let take a correct process $p_i$ that compute $M$ at line~\ref{code:Mcompute-dl}. That implies that $p_i$ has defined $\winners r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $\winners_r = \Winners_r$. \\
+  By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ sends messages to all processes at most once per round. Thus, $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined as the messages sent by $j$ in that round. Hence, when $p_i$ computes
+  \[
+    M^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
+  \]
+\end{proof}
+
+\begin{lemma}[Inclusion]\label{lem:inclusion}
+  If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ sends a proposal $S$ to all processes at line~\ref{code:submit-proposition} with $m\in S$.
+\end{lemma}
+
+\begin{proof}
+  Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the handler at line~\ref{code:abbroadcast-add}, $m$ is added to $\unordered$. Since $p_i$ is correct, it continues executing the main loop. 
+  
+  Consider any iteration of the loop where $p_i$ executes line~\ref{code:Sconstruction} while $m \in (\unordered \setminus \ordered)$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and sends $S$ to all processes at line~\ref{code:submit-proposition}.
+  
+  We distinguish two cases:
+  \begin{itemize}
+    \item \textbf{Case 1: $p_i$ is a winner.} If $p_i \in \Winners_r$ for this round $r$, then by \Cref{def:winner-invariant} and program order, $p_i$ has sent proposal $S$ to all processes with $m \in S$, and the lemma holds with $j = i$.
+    
+    \item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then $p_i$ is still a correct process, so it has sent its proposal $S$ (containing $m$) to all processes in $\Pi$. By the reliable and error-free nature of the communication channels, all correct processes will eventually receive $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\unordered$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round.
+    
+    Since there are infinitely many rounds and finitely many processes, and by \Cref{lem:nonempty} every closed round has at least one winner, there must exist a round $r'$ and a correct process $p_j \in \Winners_{r'}$ such that $m \in (\unordered \setminus \ordered)$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ sends messages $S$ with $m \in S$ at line~\ref{code:submit-proposition}.
+  \end{itemize}
+  
+  In both cases, there exists a round and a winner whose proposal includes $m$.
+\end{proof}
+
+\begin{lemma}[Broadcast Termination]\label{lem:bcast-termination}
+  A correct process which invokes $\ABbroadcast(m)$ eventually exits the function and returns.
+\end{lemma}
+
+\begin{proof}[Proof]
+  By Algorithm~\ref{alg:arb-crash}, the handler for $\ABbroadcast(m)$ at line~\ref{code:abbroadcast-add} performs a single local operation: adding $m$ to the local set $\unordered$. This operation terminates immediately and the function returns.
+\end{proof}
+
+\begin{lemma}[Validity]\label{lem:validity}
+  If a correct process $p$ invokes $\ABbroadcast(m)$, then every correct process that invokes a infinitely many times $\ABdeliver()$ eventually delivers $m$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Let $p_i$ a correct process that invokes $\ABbroadcast(m)$ and $p_q$ a correct process that infinitely invokes $\ABdeliver()$. By \Cref{lem:inclusion}, there exist a closed round $r$ and a correct process $j\in\Winners_r$ such that $p_j$ sends a proposal $S$ to all processes with $m\in S$.
+
+  By \Cref{lem:eventual-closure}, when $p_q$ computes $M$ at line~\ref{code:Mcompute-dl}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ sends messages at most once per round, so $\prop[r][j]$ is uniquely defined as the proposal sent by $j$. Hence, when $p_q$ computes
+  \[
+    M = \bigcup_{k\in\Winners_r} \prop[r][k],
+  \]
+  we have $m \in \prop[r][j] = S$, so $m \in M$. By \Cref{lem:convergence}, $M$ is invariant so each computation of $M$ by a correct process includes $m$. At each invocation of $m' = \ABdeliver()$, $m'$ is added to $\delivered$ until $M \subseteq \delivered$. Once this happens we're assured that there exists an invocation of $\ABdeliver()$ which return $m$. Hence $m$ is well delivered.
+\end{proof}
+
+\begin{lemma}[No duplication]\label{lem:no-duplication}
+  No correct process delivers the same message more than once.
+\end{lemma}
+
+\begin{proof}
+  Let consider two invokations of $\ABdeliver()$ made by the same correct process which returns $m$. Let call these two invocations respectively $\ABdeliver^{(A)}()$ and $\ABdeliver^{(B)}()$.
+
+  When $\ABdeliver^{(A)}()$ occurs, by program order and because it reached line~\ref{code:adeliver-mark} to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reached line~\ref{code:adeliver-extract} to extract the next message to deliver, it can't be $m$ because $m \not\in (\ordered \setminus \delivered)$. So a $\ABdeliver^{(B)}()$ which delivers $m$ can't occur.
+\end{proof}
+
+\begin{lemma}[Total order]\label{lem:total-order}
+  For any two messages $m_1$ and $m_2$ delivered by correct processes, if a correct process $p_i$ delivers $m_1$ before $m_2$, then any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.  
+\end{lemma}
+
+\begin{proof}
+  Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists closed rounds $r_1$ and $r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that $p_{k_1}$ and $p_{k_2}$ send proposals $S_1$ and $S_2$ respectively, with $m_1\in S_1$ and $m_2\in S_2$.
+
+  Let consider two cases :
+  \begin{itemize}
+    \item \textbf{Case 1:} $r_1 < r_2$. By program order, any correct process must have waited to append in $\delivered$ every messages in $M$ (which contains $m_1$) to increment $\current$ and eventually set $\current = r_2$ to compute $M$ and then invoke the $ m_2 = \ABdeliver()$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ before $m_2$.
+    
+    \item \textbf{Case 2:} $r_1 = r_2$. By \Cref{lem:convergence}, any correct process that computes $M$ at line~\ref{code:Mcompute-dl} computes the same set of messages $\Messages_{r_1}$. By line~\ref{code:next-msg-extraction} the messages are pull in a deterministic order defined by $\ordered(\_)$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ and $m_2$ in the deterministic order defined by $\ordered(\_)$.
+  \end{itemize}
+
+  In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ and $m_2$ in the same order.
+\end{proof}
+
+\begin{theorem}[\ARB]
+In a crash asynchronous message-passing system with reliable, error-free communication channels, assuming a synchronous DenyList ($\DL$) object, the algorithm implements Atomic Reliable Broadcast.
+\end{theorem}
+
+\begin{proof}
+  We show that the algorithm satisfies the properties of Atomic Reliable Broadcast under the assumed $\DL$ synchrony and reliable channel assumption.
+
+  First, by \Cref{lem:bcast-termination}, if a correct process invokes $\ABbroadcast(m)$, then it eventually returns from this invocation.
+  Moreover, \Cref{lem:validity} states that if a correct process invokes $\ABbroadcast(m)$, then every correct process that invokes $\ABdeliver()$ infinitely often eventually delivers $m$.
+  This gives the usual Validity property of $\ARB$.
+
+  Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from processes that constructed and sent them in the algorithm.
+  Every delivered message was previously sent by some process at line~\ref{code:submit-proposition}, so no spurious messages are delivered.
+  In addition, \Cref{lem:no-duplication} states that no correct process delivers the same message more than once.
+  Together, these arguments yield the Integrity and No-duplicates properties required by $\ARB$.
+
+  For the ordering guarantees, \Cref{lem:total-order} shows that for any two messages $m_1$ and $m_2$ delivered by correct processes, every correct process that delivers both $m_1$ and $m_2$ delivers them in the same order.
+  Hence all correct processes share a common total order on delivered messages.
+
+  All the above lemmas are proved under the assumptions that $\DL$ satisfies the required synchrony properties and that the communication channels are reliable and error-free (no message loss or corruption).
+  Therefore, under these assumptions, the algorithm satisfies Validity, Integrity/No-duplicates, and total order, and hence implements Atomic Reliable Broadcast, as claimed.
+\end{proof}
+
+\subsection{Reciprocity}
+% ------------------------------------------------------------------------------
+
+So far, we assumed the existence of a synchronous DenyList ($\DL$) object and showed how to build an Atomic Reliable Broadcast ($\ARB$) primitive using reliable, error-free point-to-point channels. We now briefly argue that, conversely, an $\ARB$ primitive is strong enough to implement a synchronous $\DL$ object.
+
+\xspace
+
+\paragraph{DenyList as a deterministic state machine.}
+Without anonymity, the \DL specification defines a
+deterministic abstract object: given a sequence $\Seq$ of operations
+$\APPEND(x)$, $\PROVE(x)$, and $\READ()$, the resulting sequence of return
+values and the evolution of the abstract state (set of appended elements,
+history of operations) are uniquely determined.
+
+\paragraph{State machine replication over \ARB.}
+Assume a system that exports a FIFO-\ARB primitive with the guarantees that if a correct process invokes $\ABbroadcast(m)$, then every correct process eventually $\ABdeliver(m)$ and the invocation eventually returns.
+Following the classical \emph{state machine replication} approach described by Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
+\begin{quote}
+  \textbf{Agreement.} Every nonfaulty state machine replica receives every request. \\
+  \textbf{Order.} Every nonfaulty state machine replica processes the requests it receives in
+  the same relative order.
+\end{quote}
+
+Which are cover by our FIFO-\ARB specification.
+
+\paragraph{Correctness.}
+
+
+\begin{theorem}[From \ARB to synchronous \DL]\label{thm:arb-to-dl}
+  In an asynchronous message-passing system with crash failures, assume a FIFO Atomic Reliable Broadcast primitive (in the standard Total Order / Atomic Broadcast sense of~\cite{Defago2004}) with Integrity, No-duplicates, Validity, and the liveness of $\ABbroadcast$. Then there exists an implementation of a DenyList object that satisfies Termination, Validity, and Anti-flickering properties.
+\end{theorem}
+
+\begin{proof}
+  Because the \DL object is deterministic, all correct processes see the same sequence of operations and compute the same sequence of states and return values. We obtain:
+
+  \begin{itemize}[leftmargin=*]
+    \item \textbf{Termination.} The liveness of \ARB ensures that each $\ABbroadcast$ invocation by a correct process eventually returns, and the corresponding operation is eventually delivered and applied at all correct processes. Thus every $\APPEND$, $\PROVE$, and $\READ$ operation invoked by a correct process eventually returns.
+    \item \textbf{APPEND/PROVE/READ Validity.} The local code that forms \ABbroadcast requests can achieve the same preconditions as in the abstract \DL specification (e.g., $p\in\Pi_M$, $x\in S$ for $\APPEND(x)$). Once an operation is delivered, its effect and return value are exactly those of the sequential \DL specification applied in the common order.
+    \item \textbf{PROVE Anti-Flickering.} In the sequential \DL specification, once an element $x$ has been appended, all subsequent $\PROVE(x)$ are invalid forever. Since all replicas apply operations in the same order, this property holds in every execution of the replicated implementation: after the first linearization point of $\APPEND(x)$, no later $\PROVE(x)$ can return valid at any correct process.
+  \end{itemize}
+
+  Formally, we can describe the \DL object with the state machine approach for
+  crash-fault, asynchronous message-passing systems with a total order broadcast
+  layer~\cite{Schneider90}.
+\end{proof}
+
+\subsubsection{Example executions}
+
+% \begin{figure}
+%   \centering
+%   \resizebox{0.4\textwidth}{!}{
+%     \input{diagrams/nonBFT_behaviour.tex}
+%   }
+%   \caption{Example execution of the ARB algorithm in a non-BFT setting}
+% \end{figure}
+
+
+% \begin{figure}
+%   \centering
+%   \resizebox{0.4\textwidth}{!}{
+%     \input{diagrams/BFT_behaviour.tex}
+%   }
+%   \caption{Example execution of the ARB algorithm with a byzantine process}
+% \end{figure}
+
+
+% font en fonctin de lusage
+
+% winner invariant
+% order invariant

Recherche/BFT-ARBover/5_BFT_ARB/index.tex

@@ -0,0 +1,559 @@
+
+\subsection{Model extension}
+We extend the crash model of Section 1 (same process universe, asynchronous setting, uniquely identifiable messages, and reliable point-to-point channels) with Byzantine faults and Byzantine-resilient dissemination primitives.
+
+\paragraph{Failure threshold.} At most $t$ processes may be Byzantine, and we assume $n > 3t$, following standard asynchronous Byzantine assumptions~\cite{Bracha87}.
+
+\paragraph{Additional communication primitive.} In addition to reliable point-to-point channels, processes use Reliable Broadcast ($\RB$) with operations $\RBcast(m)$ and $m=\rdeliver()$. We use Bracha's Byzantine RB specification~\cite{Bracha87}: for a fixed sender and broadcast instance, all correct processes that deliver, deliver the same payload, and Byzantine equivocation on that instance is prevented.
+
+\paragraph{Byzantine behaviour}
+A Byzantine process may deviate arbitrarily from the algorithm (malformed inputs, selective omission, collusion, inconsistent timing, etc.).
+
+Byzantine processes are still constrained by the assumed primitives: they cannot violate the safety/liveness guarantees of $\DL$ and cannot break the Integrity, No-duplicates, and Validity guarantees of $\RB$.
+
+
+\paragraph{Notation.} For any indice $k$ we defined by $\DL[k]$ as the $k$-th DenyList object. For a given $\DL[k]$ and any indice $x$ we defined by $\Pi_x^k$ a subset of $\Pi$. Still for a given $k$ we consider $\Pi_M^k \subseteq \Pi$ and $\Pi_V^k \subseteq \Pi$ two authorization subsets for $\DL[k]$. Indice $i \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_k$ for the $\DL[k]$ linearization: $x \prec_k y$ means that operation $x$ appears strictly before $y$ in the linearized history of $\DL[k]$. 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 operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked by process $p_i$, and by $F_i^k(...)$ the same operation invoked on the $\DL[k]$ object.
+
+% ------------------------------------------------------------------------------
+\subsection{Primitives}
+
+\subsection{Reliable Broadcast (RB)}
+
+\RB provides the following properties in this model (cf.~\cite{Bracha87}).
+\begin{itemize}[leftmargin=*]
+  \item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ m = \rbreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$.
+  \item \textbf{No-duplicates}: No message is received more than once at any process.
+  \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
+\end{itemize}
+
+\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()$ such that :
+
+\paragraph{Termination.} Every operation $\BFTAPPEND(x)$, $\BFTPROVE(x)$, and $\BFTREAD()$ invoked by a correct process always returns.
+
+\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 Liveness.} Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, x) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$.
+
+\paragraph{READ Anti-Flickering.} Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$.
+
+\paragraph{READ Safety.} Let $op_1, op_2$ respectively a valid $\BFTPROVE(x)$ operation submited by the process $p_i$ and a $\BFTREAD()$ operation submited by any correct process such that $op_1 \prec op_2$. Let $R$ the result of $op_2$ then $R \ni (i, x)$
+
+\subsection{DL $\Rightarrow$ t-BFT-DL}
+
+
+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.
+\]
+
+\[
+|\mathcal{U}| = \binom{|M|}{|M| - t}.
+\]
+
+\begin{algorithm}
+    \caption{t-BFT-DL implementation using multiple DL objects}
+
+    \Fn{$\BFTAPPEND(x)$}{
+        \For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$}{
+            $DL_U.\APPEND(x)$\;
+        }
+    }
+
+    \vspace{1em}
+
+    \Fn{$\BFTPROVE(x)$}{
+        $\state \gets false$\;
+        \For{\textbf{each } $U \in \mathcal{U}$}{
+            $\state \gets \state \textbf{ OR } DL_U.\PROVE(x)$\;\nllabel{code:prove-or}
+        }
+        \Return{$\state$}\;
+    }
+
+    \vspace{1em}
+
+    \Fn{$\BFTREAD()$}{
+        $\results \gets \emptyset$\;
+        \For{\textbf{each } $U \in \mathcal{U}$}{
+            $\results \gets \results \cup DL_U.\READ()$\;
+        }
+        \Return{$\results$}\;
+    }
+\end{algorithm}
+
+\paragraph{Algorithm intuition.}
+In the Byzantine setting, a process identifier $j$ is selected in $\winners[r]$ only when it accumulates at least $t+1$ proofs for round $r$ in $\validated(r)$. A process emits such a proof for $j$ only after receiving $j$'s $\texttt{PROP}$ payload (handler $\rdeliver(\texttt{PROP},\cdot)$). Therefore, if $j$ is a winner, at least one correct process has received $j$'s proposal. By RB agreement/validity, once one correct process receives that proposal for the instance, all correct processes eventually receive the same payload, so winner proposals eventually become available everywhere and can be merged consistently.
+
+\begin{lemma}[BFT-PROVE Validity]\label{lem:bft-prove-validity}
+    The invocation of $op = \BFTPROVE(x)$ by a correct process is invalid iff there exist at least $t+1$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$.
+\end{lemma}
+
+\begin{proof}
+    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 $\BFTAPPEND(x)$ before $op$ in $\Seq$.
+
+    \begin{itemize}
+        \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 $p_i$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $U\in\mathcal{U}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so the field $\state$ at line~\ref{code:prove-or} is never becoming true, and $op$ return false.
+
+        \item \textbf{Case (ii): $|A|\le t$.}
+        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 \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 $op$ is valid.
+    \end{itemize}
+
+    \smallskip
+    Combining the cases yields the claimed characterization of invalidity.
+\end{proof}
+
+\begin{lemma}[BFT-PROVE Anti-Flickering]\label{lem:bft-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.
+\end{lemma}
+
+\begin{proof}
+    Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$ 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$.
+
+    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.
+\end{proof}
+
+\begin{lemma}[BFT-READ Liveness]
+    Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, x) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$.
+\end{lemma}
+
+\begin{proof}
+    Let $R$ the result of a $READ()$ operation submit by any correct process. $(i, x) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, x) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, x) \in R^{U^\star}$ implie that there exist a valid  $DL_{U^\star}.\PROVE_i(x)$. The for loop in the $\BFTPROVE(x)$ implementation return true iff there at least one valid $DL_{U}.\PROVE_i(x)$ for any $U \in \mathcal{U}$.
+
+    Hence because there exist a $U^\star$ such that $DL_{U^\star}.\PROVE_i(x)$, there exist a valid $\BFTPROVE_i(x)$.
+
+     $(i, x) \in R \implies \exists \BFTPROVE_i(x)$
+\end{proof}
+
+\begin{lemma}[BFT-READ Anti-Flickering]\label{lem:bft-read-anti-flickering}
+    Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$.
+\end{lemma}
+
+\begin{proof}
+    Let $R_1, R_2$ respectively the output of two $\BFTREAD()$ operations $op_1, op_2$ such that $op_1 \prec op_2$.
+    By the implementation of $\BFTREAD$, $R_k = \bigcup_{U \in \mathcal{U}} R_k^U$ where $R_k^U$ is the result of $DL_U.\READ()$ during $op_k$.
+
+    Because $op_1 \prec op_2$ for any $U \in \mathcal{U}$, the $DL_U.\READ()$ induced by $op_1$ happen before the $DL_U.\READ()$ induced by $op_2$. Hence we have for all $U, R_2^U \subseteq R_1^U$.
+    Therefore
+    \[
+    \bigcup_U R_2^U \subseteq \bigcup_U R_1^U \implies
+    R_2 \subseteq R_1
+    \]
+\end{proof}
+
+\begin{lemma}[BFT-READ Safety]\label{lem:bft-read-safety}
+    Let $op_1, op_2$ respectively a valid $\BFTPROVE(x)$ operation submited by the process $p_i$ and a $\BFTREAD()$ operation submited by any correct process such that $op_1 \prec op_2$. Let $R$ the result of $op_2$ then $R \ni (i, x)$
+\end{lemma}
+
+\begin{proof}
+    Let $op_1 = \BFTPROVE_i(x)$ be a valid operation by a correct process $p_i$ and $op_2 = \BFTREAD()$ be any $\BFTREAD()$ operation such that $op_1 \prec op_2$ in $\Seq$.
+    By BFT-PROVE Validity, there exist at most $t$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op_1$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\le t$.
+
+    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)$ of $op_1$. Since also $i\in \Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE_i(x)$ is valid.
+
+    Now, because $op_1 \prec op_2$ in $\Seq$, the induced $DL_{U^\star}.\PROVE_i(x)$ appears before the induced $DL_{U^\star}.\READ()$ of $op_2$ in $\Seq_{U^\star}$. By \textbf{READ Safety} of $\DL$, the result $R^{U^\star}$ of the induced $DL_{U^\star}.\READ()$ contains $(i, x)$.
+
+    Finally, by the implementation of $\BFTREAD()$, we have $R = \bigcup_{U \in \mathcal{U}} R^U$, so $(i, x) \in R$.
+\end{proof}
+
+\begin{theorem}
+    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{theorem}
+
+\begin{proof}
+    Follows directly from the previous lemmas.
+\end{proof}
+
+\subsection{Algorithm}
+
+\begin{algorithm}[H]
+    \caption{t-BFT ARB at process $p_i$}\label{alg:bft-arb}
+
+    \SetKwBlock{LocalVars}{Local Variables:}{}
+    \LocalVars{
+        $\unordered \gets \emptyset$,
+        $\ordered \gets \epsilon$,
+        $\delivered \gets \epsilon$\;
+        $\prop[r][j] \gets \bot, \forall j, r \in \Pi \times \mathbb{N}$\;
+        $\done[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
+    }
+
+    \vspace{0.3em}
+
+    \For{$r = 1, 2, \ldots$}{\nllabel{alg:main-loop}
+        \textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
+        $S \gets \unordered \setminus \ordered$;
+        $\RBcast(\texttt{PROP}, S, \langle i, r \rangle)$\;
+
+        \textbf{wait until} $|\validated(r)| \geq n - t$\;\nllabel{alg:check-validated}
+
+        \BlankLine
+
+        \lForEach{$j \in \Pi$}{
+            $\BFTAPPEND(\langle j, r\rangle)$\nllabel{alg:append}
+        }
+
+        \lForEach{$j \in \Pi$}{
+            $\send(\texttt{DONE}, r)$ \textbf{ to } $p_j$
+        }
+
+        \BlankLine
+
+        \textbf{wait until} $|\done[r]| \geq n - t$\;\nllabel{alg:check-done}
+        \textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$ \textbf{ with } $\winners[r] \gets \validated(r)$\;
+
+        \BlankLine
+
+        $M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
+        $\ordered \gets \ordered \cdot \order(M)$\;
+    }
+
+    \vspace{0.3em}
+
+    \Fn{\validated($r$)}{
+        \Return{$\{j: |\{k: (k, r) \in \BFTREAD()\}| \geq t+1\}$}\;
+    }
+
+    \vspace{0.3em}
+
+    \Upon{$\ABbroadcast(m)$}{
+        $\unordered \gets \unordered \cup \{m\}$\;
+    }
+
+    \vspace{0.3em}
+
+    \Upon{$\rdeliver(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
+        $\unordered \gets \unordered \cup S$;
+        $\prop[r][j] \gets S$\;
+        $\BFTPROVE(\langle j, r\rangle)$\;
+    }
+
+    \vspace{0.3em}
+
+    \Upon{$\receive(\texttt{DONE}, r)$ from process $p_j$}{
+        $\done[r] \gets \done[r] \cup \{j\}$\;
+    }
+
+    \vspace{0.3em}
+
+    \Upon{$\ABdeliver()$}{
+        \lIf{$\ordered \setminus \delivered = \emptyset$}{
+            \Return{$\bot$}
+        }
+        let $m$ be the first message in $(\ordered \setminus \delivered)$\;
+        $\delivered \gets \delivered \cdot \{m\}$\;
+        \Return{$m$}
+    }
+    
+\end{algorithm}
+
+\paragraph{Algorithm intuition.}
+The Byzantine-tolerant construction combines threshold evidence and RB agreement to make winner selection robust. A sender $j$ appears in $\validated(r)$ only when at least $t+1$ proofs for $\langle j,r\rangle$ are observed through $\BFTREAD()$, and by \Cref{lem:bft-prove-validity} this threshold means that $j$ cannot be certified without broad enough support from the system. Once a round is closed, the winner set becomes stable by \Cref{lem:winners-stability}, so correct processes stop diverging on who contributes to the round outcome. For each stable winner, the associated proposal payload is unique at correct receivers by \Cref{lem:bft-unique-proposal}, which prevents equivocation from creating distinct local values for the same winner identity. Consequently, when correct processes wait for all winner proposals and compute the union at line~\ref{code:Mcompute}, they obtain the same message set by \Cref{lem:message-content-invariance}. Progress is then ensured by \Cref{lem:bft-eventual-closure}, which guarantees that if new messages remain unordered, a new round eventually closes with at least $n-t$ winners. Finally, once rounds are commonly closed, appending $\order(M)$ at each round yields a common delivery sequence, exactly formalized by \Cref{lem:bft-total-order}.
+
+% \textbf{Everything below has to be updated}
+
+% \begin{definition}[BFT Closed round for $k$]
+%     Given $Seq^{k}$ the linearization of the $\BFTDL$ $Y[k]$, a round $r \in \mathcal{R}$ is \emph{closed} in $\Seq$ iff there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. Let call $\BFTAPPEND(r)^\star$ the $(n-f)^{th}$ $\BFTAPPEND(r)$.
+% \end{definition}
+
+% \begin{definition}[BFT Closed round]\label{def:bft-closed-round}
+%     A round $r \in \mathcal{R}$ is \emph{closed} iff for all $\DL[k]$, $r$ is closed in $\Seq^k$.
+% \end{definition}
+
+% \subsection{Proof of correctness}
+
+% \begin{remark}[BFT Stable round closure]\label{rem:bft-stable-round-closure}
+%     If a round $r$ is closed, no more $\BFTPROVE(r)$ can be valid and thus linearized. In other words, once $\BFTAPPEND(r)^\star$ is linearized, no more process can make a proof on round $r$, and the set of valid proofs for round $r$ is fixed. Therefore $\Winners_r$ is fixed.
+% \end{remark}
+
+% \begin{proof}
+%     By definition $r$ closed means that for all process $p_i$, there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. By BFT-PROVE Validity, any subsequent $\BFTPROVE(r)$ is invalid because at least $n - f$ processes already invoked a valid $\BFTAPPEND(r)$ before it. Thus no new valid $\BFTPROVE(r)$ can be linearized after $\BFTAPPEND(r)^\star$. Hence the set of valid proofs for round $r$ is fixed, and so is $\Winners_r$.
+% \end{proof}
+
+% \begin{lemma}[BFT Across rounds]\label{lem:bft-across-rounds}
+%     For any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
+% \end{lemma}
+
+% \begin{proof}
+%     Let $r \in \mathcal{R}$. By \cref{def:bft-closed-round}, if $r + 1$ is closed, then for all $\DL[k]$, $r + 1$ is closed in $\Seq^k$. By the implementation, a process can only invoke $\BFTAPPEND(r + 1)$ after observing at least $n - f$ valid $\BFTPROVE(r)$, which means that for all $\DL[k]$, $r$ is closed in $\Seq^k$. Hence by \cref{def:bft-closed-round}, $r$ is closed.
+
+%     Because $r$ is monotonically increasing, we can reccursively apply the same argument to conclude that for any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
+% \end{proof}
+
+% \begin{lemma}[BFT Progress]\label{lem:bft_progress}
+%     For any correct process $p_i$ such that
+%     \[
+%     \received \setminus (\delivered \cup (\cup_{r' < r} \cup_{j \in W[r'] \prop[r'][j]})) \neq \emptyset
+%     \]
+%     with $r$ the highest closed round in the $\DL$ linearization. Eventually $r+1$ will be closed.
+% \end{lemma}
+
+% \begin{lemma}[BFT Winners invariant]\label{lem:bft-winners-invariant}
+%     For any closed round $r$, define
+%     \[
+%     \Winners_r = \{j: \BFTPROVE_j(r) \prec \BFTAPPEND^\star(r)\}
+%     \]
+%     called the unique set of winners of round $r$.
+% \end{lemma}
+
+% \begin{lemma}[BFT n-f lower-bounded Winners]
+%     Let $r$ a closed round, $|W[r]| \geq n-f$.
+% \end{lemma}
+
+% \begin{remark}\label{rem:correct-in-winners}
+%     Because we assume $n \geq 2f+ 1$, if $|W[r]| \geq n-f$ at least 1 correct have to be in $W[r]$ to progress.
+% \end{remark}
+
+% \begin{lemma}[BFT Winners must purpose]\label{lem:bft-winners-purpose}
+%     Let $r$ a closed round, for all process $p_j$ such that $j \in W[r]$, $p_j$ must have executed $\RBcast(j, PROP, \_, r)$ and hence any correct will eventually set $\prop[r][j]$ to a non-$\bot$ value.
+% \end{lemma}
+
+% \begin{lemma}[BFT Messages Incariant]\label{lem:bft-messages-invariant}
+%     For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r$: $\prop^{(i)}[r][j] \neq \bot$ define
+%     \[
+%         \Messages_r = \cup_{j \in \Winners_r} prop^{(i)}[r][j]
+%     \]
+%     as the set of messages proposed by the winners of round $r$
+% \end{lemma}
+
+% \begin{lemma}[BFT EVentual proposal closure]\label{lem:bft-eventual-proposal-closure}
+%     If a correct process $p_i$ define $M$ at line~\ref{code:Mcompute}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
+% \end{lemma}
+
+% \begin{lemma}[BFT Unique proposal per sender per round]\label{lem:bft-unique-proposal}
+%     For any round $r$ and any process $p_i$, if $p_i$ invokes two $\RBcast$ call for the same round, such that $\RBcast(i, PROP, S, r) \prec \RBcast(i, PROP, S', r)$. Then for any correct process $p_j$, $\prop^{(j)}[r][i] \in \{\bot, S\}$
+% \end{lemma}
+
+
+
+
+
+
+
+% \begin{lemma}[BFT $W_r$ as grow only set]\label{lem:bft-wr-grow-only}
+%     For any correct process $p_i$. If $p_i$ computes $W_r$ at two different times $t_1$ and $t_2$ with $t_1 < t_2$, then $W_r^{t_1} \subseteq W_r^{t_2}$.
+% \end{lemma}
+
+% \begin{proof}
+%     By the implementation, $W_r$ is computed exclusively from the results of $\{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$.
+
+%     We know by BFT-READ Anti-Flickering that for any two $\BFTREAD()$ operations $op_1, op_2$ such that $op_1 \prec op_2$, the result of $op_2$ is included in the result of $op_1$. Therefore, if $p_i$ computes $W_r$ at two different times $t_1$ and $t_2$ with $t_1 < t_2$, then $W_r^{t_1} \subseteq W_r^{t_2}$.
+% \end{proof}
+
+% \begin{lemma}[BFT well defined winners]\label{lem:bft-well-defined-winners}
+%     For any closed round $r$, if a correct process $p_i$ compute $W_r$, then $W_r = \Winners_r$ with $|W_r| \geq n - f$.
+% \end{lemma}
+
+% \begin{proof}
+%     By \Cref{lem:bft-read-safety}, any correct process $p_i$ computing $W_r$ after round $r$ is closed includes all valid $\BFTPROVE(r)$ in its computation of $W_r$. Therefore $W_r = \Winners_r$.
+
+%     By \Cref{def:bft-closed-round}, at least $n - f$ distinct processes invoked a valid $\BFTAPPEND(r)$ before $\BFTAPPEND(r)^\star$. By the implementation in algorithm D, if a process correct $j$ invoked a valid $\BFTAPPEND(r)$, thats means that he observed at least $n - f$ valid $\BFTPROVE(r)$ submitted by distinct processes. By \Cref{lem:bft-wr-grow-only}, once $p_j$ observed $n - f$ valid $\BFTPROVE(r)$, any correct process computing $W_r$ will eventually observe at least these $n - f$ valid $\BFTPROVE(r)$. By \Cref{lem:bft-stable-round-closure}, no more valid $\BFTPROVE(r)$ can be linearized after round $r$ is closed, so any correct process computing the same fixed set $W_r$ of at least $n - f$ distinct processes.
+% \end{proof}
+
+% \begin{lemma}[BFT Non-empty winners proposal]\label{lem:bft-non-empty-winners-proposal}
+%     For every process $p_i$ such as $i \in W_r$, eventually $\prop[r][i] \neq \bot$.
+% \end{lemma}
+
+% \begin{proof}
+%     By the implementation, if $i \in W_r$, then $(i, \PROVEtrace(r))$ is included in the result of at least one $\BFTREAD()$ operation. Hence there exist a valid $\BFTPROVE(r)$ operation.
+%     By \Cref{lem:bft-prove-validity}, this implies that there exist at least $f + 1$ valid $\PROVE(r)$ operation invoked by processes. At least one of these processes is correct, say $p_j$. By the implementation, $p_j$ invoked $\BFTPROVE(r)$ after receiving a $Rdeliver(j, \texttt{PROP}, S, r)$ message from $p_i$. Therefore, by the reliable broadcast properties, the message will eventually be delivered to every correct process, hence eventually for any correct process $\prop[r][i] \neq \bot$.
+% \end{proof}
+
+% \begin{definition}[BFT Message invariant]\label{def:bft-message-invariant}
+%     For any closed round $r$, for any correct process $p_i$, such that $\nexists j \in W_r : \prop[r][j] = \bot$, twe define the set
+%     \[
+%     \Messages_r = \bigcup_{j \in \Winners_r} \prop[r][j]
+%     \]
+%     as the unique set of messages proposed during round $r$.
+% \end{definition}
+
+% \begin{lemma}[BFT Proposal convergence]\label{lem:bft-proposal-convergence}
+%     For any closed round $r$, for any correct process $p_i$, that define $M_r$ at line B10, we have $M_r = \Messages_r$.
+% \end{lemma}
+
+% \begin{proof}
+%     By \Cref{lem:bft-well-defined-winners}, any correct process $p_i$ computing $W_r$ after round $r$ is closed has $W_r = \Winners_r$.
+%     By \Cref{lem:bft-non-empty-winners-proposal}, for any correct process $p_i$, such as $i \in W_r$, eventually $\prop[r][i] \neq \bot$.
+
+%     Therefore, eventually for any correct process $p_i$, at line B10 we have
+%     \[
+%     M_r = \bigcup_{j \in W_r} \prop[r][j] = \bigcup_{j \in \Winners_r} \prop[r][j] = \Messages_r
+%     \]
+% \end{proof}
+
+% \begin{lemma}[BFT Inclusion]\label{proof:bft-inclusion}
+%     If a correct process $p_i$ ABroadcasts a message $m$, then eventually any correct process $p_j$ ADelivers $m$.
+% \end{lemma}
+
+% \begin{proof}
+%     Let $m$ be a message ABroadcast by a correct process $p_i$ and eventually exit the \texttt{ABroadcast} function at line A10.
+
+%     By the implementation, if $p_i$ exits the \texttt{ABroadcast} function at line A10, then there exists a round $r'$ such that $m \in \prop[r'][j]$ for some $j \in W_{r'}$.
+
+%     Since $p_i$ is correct, seeing that $m \in \prop[r'][j]$ for some $j \in W_{r'}$ implies that $p_i$ received a $Rdeliver(j, \texttt{PROP}, S, r')$ message from $p_j$ such that $m \in S$. And because $p_j$ is in $W_{r'}$, at least $n - f$ correct processes invoked a valid $Y[j].\BFTPROVE(r')$ before the round $r'$ were closed. By the reliable broadcast properties, the $Rdeliver(j, \texttt{PROP}, S, r')$ message will eventually be delivered to every correct process, hence eventually for any correct process $m \in \prop[r'][j]$ with $j \in W_{r'}$. Hence $m$ will eventually be included in the set $\Messages_{r'}$ defined in \Cref{def:bft-message-invariant} and thus eventually be ADelivered by any correct process.
+% \end{proof}
+
+\subsection{Correctness Lemmas}
+
+\begin{definition}[Closed Round]
+    A round $r \in \mathcal{R}$ is said to be \emph{closed} for a correct process $p_i$ if at the moment $p_i$ computes $\winners[r]$, it satisfies $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$.
+\end{definition}
+
+\begin{lemma}[Round Monotonicity]\label{lem:round-monotonicity}
+    If a round $r$ is closed, then every round $r_1 < r$ is also closed.
+\end{lemma}
+
+\begin{proof}
+    \textbf{Base:} $r = 0$. Suppose round $1$ is closed, the set $\{r' \in \mathcal{R}: r' < r\}$ is empty, so the claim holds.
+    
+    \textbf{Inductive step:} Let $r \geq 1$. Assume that the property holds for all rounds $r' < r$: whenever round $r'$ is closed, all rounds $r_2 < r'$ are also closed. We show that if round $r$ is closed, then all rounds $r_1 < r$ are closed.
+    
+    Suppose round $r$ is closed. This means at least one correct process $p_i$ has reached line \ref{alg:check-validated} and satisfied the condition $|\validated(r)| \geq n - t$. Consequently, $p_i$ has invoked $\BFTAPPEND(\langle j, r \rangle)$ for each $j \in \Pi$ at line \ref{alg:append}. Since these operations are invoked by a correct process, and they depend on valid proofs in the byzantine fault tolerant deny list, at least one of these operations must have succeeded in the DL object.
+    
+    Moreover, by the algorithm structure, a correct process can only reach the beginning of round $r$ after completing round $r-1$. In particular, process $p_i$ reaches line \ref{alg:main-loop} for round $r$ only after having completed round $r-1$, which requires the process to have observed at least $|\done[r-1]| \geq n - t$ (line \ref{alg:check-done} for round $r-1$). This condition can only be satisfied if round $r-1$ is closed: at least $n - t$ processes must have issued DONE messages, and since $n > 3f$, at least one of these is correct.
+    
+    Since $n - t > 2f + 1$, among the $n - t$ processes satisfying the condition for round $r-1$, at least one is correct. A correct process that issued a DONE message for round $r-1$ must have previously completed its execution of lines \ref{alg:append} for round $r-1$, which in turn required observing $|\validated(r-1)| \geq n - t$ from line \ref{alg:check-validated}. Thus, round $r-1$ is closed.
+    
+    Now, considering any round $r_1 < r-1$: by the inductive hypothesis applied to round $r-1$, since round $r-1$ is closed and $r_1 < r-1$, we have that $r_1$ is also closed.
+    
+    By strong induction, if round $r$ is closed, all rounds $r_1 < r$ are closed.
+\end{proof}
+
+\begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:bft-unique-proposal}
+    For any closed round $r$ and any process $p_j \in \winners[r]$, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process $p_i$ that has received a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly this set $S_j$.
+\end{lemma}
+
+\begin{proof}
+    Let $r$ be a closed round and $p_j \in \winners[r]$. Since $j \in \winners[r]$, it means that $(j, r) \in \BFTREAD()$, i.e., at least $t+1$ distinct processes have invoked a valid $\BFTPROVE(\langle j, r \rangle)$ before the round $r$ closed.
+    
+    By the algorithm, a correct process $p_i$ invokes $\BFTPROVE(\langle j, r \rangle)$ only upon receiving a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ at line \ref{alg:append}. Let $S_j^{(i)}$ denote the set received by $p_i$.
+    
+    Since at least $t+1$ distinct processes have performed a valid $\BFTPROVE(\langle j, r \rangle)$, and since $t < n/3$, at least one of these processes is correct. Thus, at least one correct process must have received a reliable broadcast from $p_j$ for round $r$.
+    
+    Now, by Bracha's Byzantine Reliable Broadcast specification, for any message broadcast instance by process $p_j$ in round $r$, all correct processes that deliver this broadcast either receive the identical message or none at all. Formally, for all correct processes $p_i, p_i'$ that received a delivery from $p_j$ for round $r$, we have $S_j^{(i)} = S_j^{(i')}$. 
+    
+    Therefore, there exists a unique set $S_j$ such that every correct process $p_i$ that receives a reliable delivery from $p_j$ for round $r$ receives exactly $S_j$.
+\end{proof}
+
+\begin{lemma}[Winners Stability]\label{lem:winners-stability}
+    For any closed round $r$, the set $\winners[r]$ is stable.
+\end{lemma}
+
+\begin{proof}
+    Let $r$ be a closed round. By definition, a closed round $r$ means that at least one correct process $p_i$ has observed $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$ and computed $\winners[r]$ at line \ref{alg:check-done}.
+    
+    When round $r$ becomes closed, this implies that at least $n - t$ distinct processes have invoked $\BFTAPPEND(\langle j, r \rangle)$ for $j \in \Pi$ (by the algorithm structure, since $\done[r]$ contains DONE messages from processes that completed line \ref{alg:append}). Since $n > 3f$, we have $n - t > 2f + 1 > t + 1$.
+    
+    Consider a fixed $j \in \Pi$. Since at least $n - t > t + 1$ processes have invoked a valid $\BFTAPPEND(\langle j, r \rangle)$, by \cref{lem:bft-prove-validity}, any subsequent invocation of $\BFTPROVE(\langle j, r \rangle)$ will be invalid.
+    
+    By \cref{lem:bft-prove-anti-flickering}, once a $\BFTPROVE(\langle j, r \rangle)$ operation becomes invalid, all subsequent $\BFTPROVE(\langle j, r \rangle)$ operations are also invalid.
+    
+    This holds for all $j \in \Pi$. Therefore, after the round $r$ is closed, the set of valid $\BFTPROVE(\langle j, r \rangle)$ operations for each $j$ cannot grow. By \cref{lem:bft-read-anti-flickering}, any subsequent $\BFTREAD()$ invocation will not return any new $(k, r)$ pairs beyond those already returned. Thus, $\winners[r] = \{j : (j, r) \in \BFTREAD()\}$ becomes stable and cannot change.
+    
+    Since this reasoning applies to all correct processes that compute $\winners[r]$ after round $r$ is closed, all correct processes will compute the same stable set $\winners[r]$.
+\end{proof}
+
+\begin{lemma}[Message Content Invariance]\label{lem:message-content-invariance}
+    For any closed round $r$ and any correct process $p_i$, the set $M$ computed at line \ref{code:Mcompute} by $p_i$ is identical to the set computed by any other correct process $p_j$ for the same round $r$.
+\end{lemma}
+
+\begin{proof}
+    Let $r$ be a closed round and let $p_i, p_{i'}$ be two correct processes. By the algorithm, both processes compute $M$ as:
+    \[
+    M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j]
+    \]
+    and
+    \[
+    M^{(i')} = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j]
+    \]
+    at line \ref{code:Mcompute}.
+    
+    By \cref{lem:winners-stability}, the set $\winners[r]$ is stable once round $r$ is closed. Therefore, both $p_i$ and $p_{i'}$ compute the same set of winners $\winners[r]$.
+    
+    Now, consider any winner $j \in \winners[r]$. By \cref{lem:bft-unique-proposal}, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process that receives a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly $S_j$. 
+    
+    By the algorithm, each correct process stores this received set in its local variable: $\prop^{(i)}[r][j] = S_j$ and $\prop^{(i')}[r][j] = S_j$.
+    
+    Since both processes compute the union over the same set of winners, and each winner's proposal is identical for all correct processes:
+    \[
+    M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j] = \bigcup_{j \in \winners[r]} S_j = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j] = M^{(i')}
+    \]
+    
+    Therefore, all correct processes compute the same set $M$ for any closed round $r$.
+\end{proof}
+
+\begin{lemma}[Inclusion]\label{lem:bft-inclusion}
+    If a correct process $p_i$ invokes $\ABbroadcast(m)$, then there exist a closed round $r$ and a winner $j \in \winners[r]$ such that $p_j$ invoked $\RBcast(j, \texttt{PROP}, S, r)$ with $m \in S$.
+\end{lemma}
+
+\begin{proof}
+    Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the algorithm, $p_i$ adds $m$ to $\unordered$. Consequently, $\unordered \setminus \ordered \neq \emptyset$, and the process enters the main loop and eventually invokes $\RBcast(i, \texttt{PROP}, S_i^{(1)}, r_1)$ for some round $r_1$ where $m \in S_i^{(1)}$.
+
+    We distinguish two cases:
+    
+    \textbf{Case 1: $p_i$ becomes a winner in round $r_1$.}
+    If $p_i$ is elected as a winner for round $r_1$ (i.e., $i \in \winners[r_1]$), then the claim holds with $r = r_1$ and $j = i$.
+    
+    \textbf{Case 2: $p_i$ does not become a winner in round $r_1$.}
+    If $p_i$ is not elected as a winner, by the properties of Reliable Broadcast (Bracha's specification), at least one correct process $p_{i_1}$ will eventually receive the reliable delivery of the $\texttt{PROP}$ message from $p_i$ for round $r_1$. Process $p_{i_1}$ adds all messages from $S_i^{(1)}$ to its $\unordered$ set at line \ref{alg:append}. In particular, $m$ is now in $p_{i_1}$'s $\unordered$ set.
+    
+    In round $r_2 > r_1$ (and any subsequent round), process $p_{i_1}$ computes $S_{i_1}^{(2)} = \unordered \setminus \ordered$ and invokes $\RBcast(i_1, \texttt{PROP}, S_{i_1}^{(2)}, r_2)$ with $m \in S_{i_1}^{(2)}$.
+    
+    This process repeats: either $p_{i_1}$ becomes a winner and the claim holds, or another correct process receives $p_{i_1}$'s proposal and includes $m$ in its own proposal.
+    
+    Since $n > 3f$, we have $n - t > t + 1 > f$. By the pigeonhole principle, there eventually exists a round $r$ where at least $n - t$ distinct processes have proposed sets containing $m$. Since more than $2f$ processes have proposed $m$, at least one of them must be correct and be elected as a winner. Therefore, there exist a round $r$ and a winner $j \in \winners[r]$ such that $m \in S_j$ was broadcast by $p_j$.
+\end{proof}
+
+\begin{lemma}[Eventual Closure]\label{lem:bft-eventual-closure}
+    For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$.
+\end{lemma}
+
+\begin{proof}
+    Let $p_i$ be a correct process such that $\unordered \setminus \ordered \neq \emptyset$ after round $r$ is the highest closed round it observed. By the main loop of Algorithm~\ref{alg:bft-arb}, $p_i$ eventually enters round $r+1$, computes $S=\unordered\setminus\ordered$, and invokes $\RBcast(\texttt{PROP},S,\langle i,r+1\rangle)$.
+
+    By RB Validity, every correct process eventually $\rdeliver(\texttt{PROP},S,\langle i,r+1\rangle)$. Upon this delivery, each correct process executes $\BFTPROVE(\langle i,r+1\rangle)$. Hence at least $n-t$ correct processes issue a proof for candidate $i$ in round $r+1$, and in particular the threshold $t+1$ used in $\validated(r+1)$ is eventually met for that candidate.
+
+    The same argument applies to each correct process that broadcasts in round $r+1$: once its proposal is RB-delivered, at least $n-t$ correct processes issue the corresponding proofs, so that sender is eventually included in $\validated(r+1)$. Since there are at least $n-t$ correct processes, eventually $|\validated(r+1)| \geq n-t$, and the wait at line~\ref{alg:check-validated} is eventually released for every correct process in that round.
+
+    After this point, each correct process executes the $\BFTAPPEND$ loop (line~\ref{alg:append}) and sends $\texttt{DONE}$ to all processes. By reliability of point-to-point channels, every correct process eventually receives at least $n-t$ DONE messages, so the wait at line~\ref{alg:check-done} is also eventually released. At that moment, the process computes $\winners[r+1] \gets \validated(r+1)$, and by the previous bound we have $|\winners[r+1]| \geq n-t$.
+
+    Therefore round $r+1$ eventually becomes closed with at least $n-t$ winners.
+\end{proof}
+
+\begin{lemma}[Total Order]\label{lem:bft-total-order}
+    For any two correct processes $p_i$ and $p_j$, the sequence $\ordered$ maintained locally by $p_i$ and the sequence maintained by $p_j$ contain the same messages in the same order, provided that both have reached the same set of closed rounds.
+\end{lemma}
+
+\begin{proof}
+    We prove the claim by induction on the number of closed rounds completed by both processes.
+
+    \textbf{Base case.} Before any closed round is completed, both local sequences are initialized to $\epsilon$, hence identical.
+
+    \textbf{Induction step.} Assume that after all closed rounds up to $r-1$, processes $p_i$ and $p_j$ have identical $\ordered$ prefixes. Consider round $r$.
+
+    By \Cref{lem:winners-stability}, once round $r$ is closed, both processes use the same stable winner set $\winners[r]$. By \Cref{lem:message-content-invariance}, the set $M$ computed at line~\ref{code:Mcompute} is identical at all correct processes for that round. Both processes then apply the same deterministic ordering function $\order(M)$ and append that same ordered block to their current sequence.
+
+    Since they started round $r$ from identical prefixes and append the same ordered suffix for round $r$, their resulting sequences after round $r$ are identical. The induction concludes that for any common set of closed rounds, both correct processes maintain the same messages in the same order.
+\end{proof}
+
+\begin{theorem}
+    The algorithm implements a BFT Atomic Reliable Broadcast.
+\end{theorem}

docs/presentations/autre/WinterSchoolGDRCyber2026/convergence_hc.tex

@@ -0,0 +1,41 @@
+\resizebox{\columnwidth}{!}{
+    \begin{tikzpicture}[
+        roundnode/.style={circle, draw=black, fill=black, very thick, minimum size=1pt,},
+        ignorednode/.style={circle, draw=black!20, fill=black!20, very thick, minimum size=1pt,},
+        arrow/.style={|->, thick,},
+        message/.style={->, blue!50, dashed, -{Circle[length=4pt,]}},
+        ]
+
+        \node[roundnode] (11) {};
+        \node[left] at (11.west) {$p_0$};
+        \node[above] at (11.north) {$w(1)$};
+        \node[roundnode] (12) [right=of 11] {};
+        \node[above] at (12.north) {$I(a)$};
+        \node[roundnode] (13) [right=of 12] {};
+        \node[above] at (13.north) {$r/(0,1)$};
+        \node[roundnode] (14) [right=35pt of 13] {};
+        \node[above] at (14.north) {$r/(1,2)^w$};
+
+        \draw[arrow] (11) -- (12);
+        \draw[arrow] (12) -- (13);
+        \draw[arrow] (13) -- (14);
+
+        \node[roundnode] (21) [below=of 11] {};
+        \node[left] at (21.west) {$p_1$};
+        \node[below] at (21.south) {$w(2)$};
+        \node[roundnode] (22) [right=of 21] {};
+        \node[below] at (22.south) {$R/\emptyset$};
+        \node[roundnode] (23) [right=of 22] {};
+        \node[below] at (23.south) {$r/(0,2)$};
+        \node[roundnode] (24) [right=35pt of 23] {};
+        \node[below] at (24.south) {$r/(1,2)^w$};
+
+        \draw[arrow] (21) -- (22);
+        \draw[arrow] (22) -- (23);
+        \draw[arrow] (23) -- (24);
+
+        \draw (24) -- (14);
+
+        \draw[dashed] ($(14)!0.5!(13) + (0,1)$) -- ++(0, -3.5);
+    \end{tikzpicture}
+}

docs/presentations/autre/WinterSchoolGDRCyber2026/images/logo-amu.svg

@@ -0,0 +1,42 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<svg id="Calque_2" data-name="Calque 2" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 272.51 118.06">
+  <defs>
+    <style>
+      .cls-1 {
+        fill: #fff;
+        stroke-width: 0px;
+      }
+    </style>
+  </defs>
+  <g id="Calque_1-2" data-name="Calque 1-2">
+    <g>
+      <path class="cls-1" d="M66.58,96.69c-2.35.41-4.83.55-7.73.55-7.6,0-11.74-3.59-12.43-10.77-3.87,7.87-11.6,11.88-23.2,11.88S0,91.57,0,78.45c0-14.23,11.05-18.79,23.48-21.13l22.79-4.42c0-6.77-.28-9.94-2.35-12.57-1.8-2.76-6.49-4.56-12.57-4.56-12.02,0-16.85,4.42-16.85,14.92l-12.15-1.66c.41-8.29,3.18-14.5,8.56-17.96,4.97-3.31,12.29-5.11,21.13-5.11,17.27,0,26.24,7.73,26.24,22.79v33.01c0,4.01.14,5.25,4.01,5.25,1.1,0,2.49-.14,4.01-.55l.28,10.22h0ZM46.28,62.16l-20.86,4.56c-8.01,1.79-12.71,4.01-12.71,11.6,0,6.22,5.39,10.08,12.43,10.08,14.36,0,21.13-7.18,21.13-17.82v-8.43h0Z"/>
+      <path class="cls-1" d="M180.52,96.69h-12.71v-40.61c0-8.15-.14-11.88-4.14-16.02-3.32-3.32-7.32-3.87-11.6-3.87-4.01,0-7.46,1.24-10.22,3.73-4.01,3.45-6.35,8.56-6.35,18.65v38.12h-12.71v-40.61c0-8.15-.14-11.88-4.14-16.02-3.31-3.32-7.6-3.87-11.6-3.87s-7.32,1.24-10.22,3.73c-3.87,3.45-6.35,8.56-6.35,18.65v38.12h-12.29V27.62h12.29v10.5c.97-2.62,2.76-4.97,5.11-6.91,4.28-3.45,9.67-5.25,16.16-5.25,10.91,0,18.78,5.25,22.1,14.64,1.52-3.73,3.45-6.49,6.63-9.39,3.87-3.32,8.43-5.25,16.16-5.25,15.47,0,23.89,8.84,23.89,25.97v44.75h0Z"/>
+      <path class="cls-1" d="M196.96,0h12.57v64.78c0,14.92,11.33,22.51,25.14,22.51s25.28-7.6,25.28-22.51V0h12.57v64.78c0,21.69-13.4,33.56-37.85,33.56s-37.71-11.88-37.71-33.56V0h0Z"/>
+    </g>
+    <g>
+      <path class="cls-1" d="M10,114.14h-5.27l-1.37,3.71h-1.7l4.86-12.42h1.7l4.84,12.42h-1.69l-1.38-3.71h0ZM9.47,112.72l-1.4-3.74c-.28-.75-.51-1.42-.71-2h-.02c-.16.51-.39,1.17-.69,2l-1.38,3.74h4.21-.01Z"/>
+      <path class="cls-1" d="M14.29,105.43h1.6v1.88h-1.6v-1.88ZM14.29,108.98h1.6v8.87h-1.6v-8.87Z"/>
+      <path class="cls-1" d="M25.45,117.85h-1.72l-1.47-2.09c-.25-.37-.5-.76-.76-1.21l-.2-.3c-.41.66-.73,1.17-.98,1.51l-1.47,2.09h-1.72l3.32-4.63-3.05-4.24h1.72l1.44,2,.75,1.15.16-.23c.14-.23.34-.53.6-.92l1.4-2h1.74l-3.09,4.24,3.34,4.63h-.01Z"/>
+      <path class="cls-1" d="M78.17,105.43h2.32l2.63,7.03c.51,1.37.94,2.55,1.28,3.6h.02c.39-1.19.82-2.38,1.26-3.6l2.63-7.03h2.32v12.42h-1.58v-7.51c0-.3,0-.75.02-1.29l.07-1.54h-.02c-.46,1.33-.8,2.29-1.01,2.84l-2.89,7.51h-1.63l-2.89-7.51c-.16-.41-.5-1.35-1.01-2.84h-.02l.05,1.54c.02.55.04.99.04,1.29v7.51h-1.58v-12.42h0Z"/>
+      <path class="cls-1" d="M101.14,117.85c-.3.05-.62.07-.99.07-.98,0-1.51-.46-1.6-1.38-.5,1.01-1.49,1.53-2.98,1.53s-2.98-.87-2.98-2.56c0-1.83,1.42-2.41,3.02-2.71l2.93-.57c0-.87-.04-1.28-.3-1.62-.23-.36-.83-.59-1.61-.59-1.54,0-2.17.57-2.17,1.92l-1.56-.21c.05-1.07.41-1.86,1.1-2.31.64-.43,1.58-.66,2.71-.66,2.22,0,3.37.99,3.37,2.93v4.24c0,.51.02.67.51.67.14,0,.32-.02.51-.07l.04,1.31h0ZM98.53,113.41l-2.68.59c-1.03.23-1.63.51-1.63,1.49,0,.8.69,1.3,1.6,1.3,1.85,0,2.72-.92,2.72-2.29v-1.08h-.01Z"/>
+      <path class="cls-1" d="M107.55,110.27c-.07-.02-.21-.02-.41-.02-1.81,0-2.91.62-2.91,3.39v4.21h-1.6v-8.87h1.6v1.56c.25-.87,1.35-1.65,2.77-1.76.09-.02.28-.02.59-.02l-.04,1.51h0Z"/>
+      <path class="cls-1" d="M109.5,114.8c0,1.24.87,2.01,2.27,2.01,1.47,0,2.18-.5,2.18-1.44-.07-.82-.8-.98-2.15-1.3l-.71-.16c-1.76-.48-2.77-.85-2.86-2.56,0-1.77,1.62-2.59,3.28-2.59,2.06,0,3.55.87,3.71,2.91l-1.49.23c-.02-1.21-.82-1.88-2.24-1.88-.89,0-1.77.44-1.77,1.22.09.78.8.98,2.13,1.28l.21.05c.76.16,1.35.32,1.79.48.91.3,1.6.96,1.6,2.22,0,.99-.35,1.7-1.05,2.15-.69.43-1.56.64-2.61.64-2.08,0-3.76-.98-3.76-3.12l1.46-.14h.01Z"/>
+      <path class="cls-1" d="M125.2,113.89h-6.73c.05,1.97.87,2.89,2.52,2.89,1.51,0,2.32-.64,2.54-1.99l1.54.12c-.41,2.06-1.79,3.14-4.06,3.14-1.38,0-2.45-.43-3.19-1.29-.73-.8-1.08-1.93-1.08-3.37,0-1.33.39-2.47,1.12-3.3.78-.87,1.86-1.33,3.14-1.33,1.42,0,2.75.62,3.46,1.76.48.76.76,1.86.76,3,0,.16,0,.28-.02.37ZM118.49,112.59h5.08c-.02-.5-.2-1.17-.48-1.58-.44-.66-1.1-.96-2.08-.96s-1.74.37-2.09.96c-.28.5-.41,1.06-.43,1.58Z"/>
+      <path class="cls-1" d="M127.01,105.43h1.6v1.88h-1.6v-1.88ZM127.01,108.98h1.6v8.87h-1.6v-8.87Z"/>
+      <path class="cls-1" d="M130.94,105.43h1.6v12.42h-1.6v-12.42Z"/>
+      <path class="cls-1" d="M134.88,105.43h1.6v12.42h-1.6v-12.42Z"/>
+      <path class="cls-1" d="M146.77,113.89h-6.73c.05,1.97.87,2.89,2.52,2.89,1.51,0,2.32-.64,2.54-1.99l1.54.12c-.41,2.06-1.79,3.14-4.06,3.14-1.38,0-2.45-.43-3.19-1.29-.73-.8-1.08-1.93-1.08-3.37,0-1.33.39-2.47,1.12-3.3.78-.87,1.86-1.33,3.14-1.33,1.42,0,2.75.62,3.46,1.76.48.76.76,1.86.76,3,0,.16,0,.28-.02.37h0ZM140.06,112.59h5.08c-.02-.5-.2-1.17-.48-1.58-.44-.66-1.1-.96-2.08-.96s-1.74.37-2.09.96c-.28.5-.41,1.06-.43,1.58h0Z"/>
+      <path class="cls-1" d="M196.95,105.43h1.62v8.32c0,1.92,1.46,2.89,3.23,2.89s3.25-.98,3.25-2.89v-8.32h1.61v8.32c0,2.79-1.72,4.31-4.86,4.31s-4.84-1.53-4.84-4.31v-8.32h0Z"/>
+      <path class="cls-1" d="M216.59,117.85h-1.65v-5.18c0-1.06-.02-1.49-.53-2.06-.44-.44-.92-.51-1.58-.51-.59,0-1.12.2-1.6.6-.48.39-.71,1.14-.71,2.25v4.9h-1.6v-8.87h1.6v1.37c.46-1.05,1.37-1.58,2.73-1.58,1.15,0,2,.3,2.64.99.66.76.69,1.61.69,2.82v5.27h.01Z"/>
+      <path class="cls-1" d="M218.84,105.43h1.6v1.88h-1.6v-1.88ZM218.84,108.98h1.6v8.87h-1.6v-8.87Z"/>
+      <path class="cls-1" d="M221.74,108.98h1.7l1.58,4.6c.2.51.48,1.46.89,2.8.32-1.07.62-2.01.91-2.8l1.6-4.6h1.67l-3.32,8.87h-1.7l-3.32-8.87h0Z"/>
+      <path class="cls-1" d="M238.96,113.89h-6.73c.05,1.97.87,2.89,2.52,2.89,1.51,0,2.33-.64,2.54-1.99l1.54.12c-.41,2.06-1.79,3.14-4.06,3.14-1.38,0-2.45-.43-3.19-1.29-.73-.8-1.08-1.93-1.08-3.37,0-1.33.39-2.47,1.12-3.3.78-.87,1.86-1.33,3.14-1.33,1.42,0,2.75.62,3.46,1.76.48.76.76,1.86.76,3,0,.16,0,.28-.02.37h0ZM232.25,112.59h5.08c-.02-.5-.2-1.17-.48-1.58-.44-.66-1.1-.96-2.08-.96s-1.74.37-2.09.96c-.28.5-.41,1.06-.43,1.58h0Z"/>
+      <path class="cls-1" d="M245.69,110.27c-.07-.02-.21-.02-.41-.02-1.81,0-2.91.62-2.91,3.39v4.21h-1.6v-8.87h1.6v1.56c.25-.87,1.35-1.65,2.77-1.76.09-.02.28-.02.59-.02l-.04,1.51Z"/>
+      <path class="cls-1" d="M247.64,114.8c0,1.24.87,2.01,2.27,2.01,1.47,0,2.18-.5,2.18-1.44-.07-.82-.8-.98-2.15-1.3l-.71-.16c-1.76-.48-2.77-.85-2.86-2.56,0-1.77,1.62-2.59,3.28-2.59,2.06,0,3.55.87,3.71,2.91l-1.49.23c-.02-1.21-.82-1.88-2.24-1.88-.89,0-1.78.44-1.78,1.22.09.78.8.98,2.13,1.28l.21.05c.76.16,1.35.32,1.79.48.91.3,1.6.96,1.6,2.22,0,.99-.35,1.7-1.05,2.15-.69.43-1.56.64-2.61.64-2.08,0-3.76-.98-3.76-3.12l1.46-.14h.02Z"/>
+      <path class="cls-1" d="M255.39,105.43h1.6v1.88h-1.6v-1.88h0ZM255.39,108.98h1.6v8.87h-1.6v-8.87h0Z"/>
+      <path class="cls-1" d="M259.82,110.31h-1.28v-1.33h1.28v-2.47h1.58v2.47h1.81v1.33h-1.81v5.5c0,.57.23.69.92.69.21,0,.48-.04.82-.09l.04,1.44c-.39.05-.71.09-.98.09-1.65,0-2.38-.64-2.38-2.08v-5.55Z"/>
+      <path class="cls-1" d="M272.47,113.89h-6.73c.05,1.97.87,2.89,2.52,2.89,1.51,0,2.32-.64,2.54-1.99l1.54.12c-.41,2.06-1.79,3.14-4.06,3.14-1.38,0-2.45-.43-3.19-1.29-.73-.8-1.08-1.93-1.08-3.37,0-1.33.39-2.47,1.12-3.3.78-.87,1.86-1.33,3.14-1.33,1.42,0,2.75.62,3.46,1.76.48.76.76,1.86.76,3,0,.16,0,.28-.02.37h0ZM265.76,112.59h5.08c-.02-.5-.2-1.17-.48-1.58-.44-.66-1.1-.96-2.08-.96s-1.74.37-2.09.96c-.28.5-.41,1.06-.43,1.58ZM268.63,105.42h1.79l-1.63,2.25h-1.31l1.15-2.25Z"/>
+    </g>
+  </g>
+</svg>

docs/presentations/autre/WinterSchoolGDRCyber2026/images/logo-lis-2024.svg

@@ -0,0 +1,37 @@
+<?xml version="1.0"?>
+<svg width="660" height="510" xmlns="http://www.w3.org/2000/svg" xmlns:svg="http://www.w3.org/2000/svg" preserveAspectRatio="xMidYMid meet" version="1.0">
+ <defs id="defs939">
+  <rect height="39.84" id="rect1474" width="107.41" x="416.03" y="533.27"/>
+ </defs>
+ <metadata id="metadata887">Created by potrace 1.16, written by Peter Selinger 2001-2019image/svg+xml</metadata>
+ <g class="layer">
+  <title>Layer 1</title>
+  <g fill="#000000" id="g933" transform="matrix(0.1, 0, 0, -0.1, -2.91941e-08, 784)">
+   <path d="m80,6590l0,-1190l735,0l735,0l0,225l0,225l-510,0l-510,0l0,965l0,965l-225,0l-225,0l0,-1190z" id="path889"/>
+   <path d="m4780,7270l0,-510l220,0l220,0l0,290l0,290l515,0l515,0l0,220l0,220l-735,0l-735,0l0,-510z" id="path891"/>
+   <path d="m2940,6085l0,-685l225,0l225,0l0,685l0,685l-225,0l-225,0l0,-685z" id="path893"/>
+   <path d="m5800,6310l0,-460l-510,0l-510,0l0,-225l0,-225l735,0l735,0l0,685l0,685l-225,0l-225,0l0,-460z" id="path895"/>
+   <path d="m6410,2980l0,-70l-135,0l-135,0l0,-60l0,-60l195,0l195,0l0,130l0,130l-60,0l-60,0l0,-70z" id="path931"/>
+  </g>
+  <text fill="#000000" font-family="sans-serif" font-size="30px" font-style="normal" font-weight="normal" id="text1544" stroke-width="0.75" x="359.79" xml:space="preserve" y="543.86"/>
+  <g id="g1632">
+   <text fill="#73c6cb" font-family="sans-serif" font-size="30px" font-style="normal" font-weight="normal" id="text1540" letter-spacing="12.58px" stroke-width="0.75" x="288.59" xml:space="preserve" y="339.91">
+    <tspan dx="0 0 0 2.8299999 1.16 0 -1.11 0.51999998 0 0.73000008 -2.25" fill="#73c6cb" font-family="&#x27;Avenir Next&#x27;, &#x27;Avenir Next LT Pro&#x27;, sans-serif" font-style="normal" font-weight="bold" id="tspan1538" stroke-width="0.75" x="288.59" y="339.91">LABORATOIRE</tspan>
+   </text>
+   <rect fill="#73c6cb" height="60.02" id="rect1534" opacity="1" stroke-linejoin="round" stroke-width="0.31" width="45.01" x="293.36" y="6.69"/>
+   <rect fill="#73c6cb" height="12.87" id="rect1536" opacity="1" stroke-linejoin="round" stroke-width="0.29" width="12" x="641" y="468.13"/>
+   <text fill="#888888" fill-opacity="0.97" font-family="sans-serif" font-size="24.2px" font-style="normal" font-weight="normal" id="text1578" stroke-width="0.6" x="479.48" xml:space="preserve" y="506.07">
+    <tspan dx="0 1.62 1.84 0 -1.1900001 0 0.20999999 -0.19" fill="#888888" fill-opacity="0.97" id="tspan1576" stroke-width="0.6" x="479.48" y="506.07">UMR 7020</tspan>
+   </text>
+   <g id="g877" transform="translate(6)">
+    <text fill="#000000" font-family="sans-serif" font-size="30px" font-style="normal" font-weight="normal" id="text1572" letter-spacing="10.99px" stroke-width="0.77" transform="translate(449.685, -4.02411) scale(0.97553, 1.02508)" x="-106.04" xml:space="preserve" y="434.98">
+     <tspan dx="-101 0 0 0 0 0 0 3.6500001 2.2551844 1.2095989" fill="#000000" font-family="&#x27;Avenir Next&#x27;, &#x27;Avenir Next LT Pro&#x27;, sans-serif" font-size="30px" id="tspan1570" stroke-width="0.77" x="-114.04" y="434.98">&amp; DES SYSTÈMES</tspan>
+    </text>
+    <text fill="#000000" font-family="sans-serif" font-size="30.3px" font-style="normal" font-weight="normal" id="text1540-5" letter-spacing="11.23px" stroke-width="0.77" transform="translate(449.685, -4.02411) scale(0.975654, 1.02495)" x="-248.22" xml:space="preserve" y="386.02">
+     <tspan dx="0 1.25 0 0.15000001 2.3599999 3.6400001 2.6099999 1.1799999 3.26 0 0 -0.46000001 3.27 0.94" fill="#000000" font-family="&#x27;Avenir Next&#x27;, &#x27;Avenir Next LT Pro&#x27;, sans-serif" font-size="30.3px" font-style="normal" font-weight="normal" id="tspan1538-1" stroke-width="0.77" x="-248.22" y="386.02">D&#x27;INFORMATIQUE</tspan>
+    </text>
+   </g>
+   <text font-family="sans-serif" font-size="30px" id="text1472" letter-spacing="9.19px" x="289.68" xml:space="preserve" y="-139.02"/>
+  </g>
+ </g>
+</svg>

docs/presentations/autre/WinterSchoolGDRCyber2026/images/logo_AMU.svg

@@ -0,0 +1,42 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<svg id="Calque_2" data-name="Calque 2" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 272.51 118.06">
+  <defs>
+    <style>
+      .cls-1 {
+        fill: #1e64de;
+        stroke-width: 0px;
+      }
+    </style>
+  </defs>
+  <g id="Calque_1-2" data-name="Calque 1-2">
+    <g>
+      <path class="cls-1" d="M66.58,96.69c-2.35.41-4.83.55-7.73.55-7.6,0-11.74-3.59-12.43-10.77-3.87,7.87-11.6,11.88-23.2,11.88S0,91.57,0,78.45c0-14.23,11.05-18.79,23.48-21.13l22.79-4.42c0-6.77-.28-9.94-2.35-12.57-1.8-2.76-6.49-4.56-12.57-4.56-12.02,0-16.85,4.42-16.85,14.92l-12.15-1.66c.41-8.29,3.18-14.5,8.56-17.96,4.97-3.31,12.29-5.11,21.13-5.11,17.27,0,26.24,7.73,26.24,22.79v33.01c0,4.01.14,5.25,4.01,5.25,1.1,0,2.49-.14,4.01-.55l.28,10.22h0ZM46.28,62.16l-20.86,4.56c-8.01,1.79-12.71,4.01-12.71,11.6,0,6.22,5.39,10.08,12.43,10.08,14.36,0,21.13-7.18,21.13-17.82v-8.43h0Z"/>
+      <path class="cls-1" d="M180.52,96.69h-12.71v-40.61c0-8.15-.14-11.88-4.14-16.02-3.32-3.32-7.32-3.87-11.6-3.87-4.01,0-7.46,1.24-10.22,3.73-4.01,3.45-6.35,8.56-6.35,18.65v38.12h-12.71v-40.61c0-8.15-.14-11.88-4.14-16.02-3.31-3.32-7.6-3.87-11.6-3.87s-7.32,1.24-10.22,3.73c-3.87,3.45-6.35,8.56-6.35,18.65v38.12h-12.29V27.62h12.29v10.5c.97-2.62,2.76-4.97,5.11-6.91,4.28-3.45,9.67-5.25,16.16-5.25,10.91,0,18.78,5.25,22.1,14.64,1.52-3.73,3.45-6.49,6.63-9.39,3.87-3.32,8.43-5.25,16.16-5.25,15.47,0,23.89,8.84,23.89,25.97v44.75h0Z"/>
+      <path class="cls-1" d="M196.96,0h12.57v64.78c0,14.92,11.33,22.51,25.14,22.51s25.28-7.6,25.28-22.51V0h12.57v64.78c0,21.69-13.4,33.56-37.85,33.56s-37.71-11.88-37.71-33.56V0h0Z"/>
+    </g>
+    <g>
+      <path class="cls-1" d="M10,114.14h-5.27l-1.37,3.71h-1.7l4.86-12.42h1.7l4.84,12.42h-1.69l-1.38-3.71h0ZM9.47,112.72l-1.4-3.74c-.28-.75-.51-1.42-.71-2h-.02c-.16.51-.39,1.17-.69,2l-1.38,3.74h4.21-.01Z"/>
+      <path class="cls-1" d="M14.29,105.43h1.6v1.88h-1.6v-1.88ZM14.29,108.98h1.6v8.87h-1.6v-8.87Z"/>
+      <path class="cls-1" d="M25.45,117.85h-1.72l-1.47-2.09c-.25-.37-.5-.76-.76-1.21l-.2-.3c-.41.66-.73,1.17-.98,1.51l-1.47,2.09h-1.72l3.32-4.63-3.05-4.24h1.72l1.44,2,.75,1.15.16-.23c.14-.23.34-.53.6-.92l1.4-2h1.74l-3.09,4.24,3.34,4.63h-.01Z"/>
+      <path class="cls-1" d="M78.17,105.43h2.32l2.63,7.03c.51,1.37.94,2.55,1.28,3.6h.02c.39-1.19.82-2.38,1.26-3.6l2.63-7.03h2.32v12.42h-1.58v-7.51c0-.3,0-.75.02-1.29l.07-1.54h-.02c-.46,1.33-.8,2.29-1.01,2.84l-2.89,7.51h-1.63l-2.89-7.51c-.16-.41-.5-1.35-1.01-2.84h-.02l.05,1.54c.02.55.04.99.04,1.29v7.51h-1.58v-12.42h0Z"/>
+      <path class="cls-1" d="M101.14,117.85c-.3.05-.62.07-.99.07-.98,0-1.51-.46-1.6-1.38-.5,1.01-1.49,1.53-2.98,1.53s-2.98-.87-2.98-2.56c0-1.83,1.42-2.41,3.02-2.71l2.93-.57c0-.87-.04-1.28-.3-1.62-.23-.36-.83-.59-1.61-.59-1.54,0-2.17.57-2.17,1.92l-1.56-.21c.05-1.07.41-1.86,1.1-2.31.64-.43,1.58-.66,2.71-.66,2.22,0,3.37.99,3.37,2.93v4.24c0,.51.02.67.51.67.14,0,.32-.02.51-.07l.04,1.31h0ZM98.53,113.41l-2.68.59c-1.03.23-1.63.51-1.63,1.49,0,.8.69,1.3,1.6,1.3,1.85,0,2.72-.92,2.72-2.29v-1.08h-.01Z"/>
+      <path class="cls-1" d="M107.55,110.27c-.07-.02-.21-.02-.41-.02-1.81,0-2.91.62-2.91,3.39v4.21h-1.6v-8.87h1.6v1.56c.25-.87,1.35-1.65,2.77-1.76.09-.02.28-.02.59-.02l-.04,1.51h0Z"/>
+      <path class="cls-1" d="M109.5,114.8c0,1.24.87,2.01,2.27,2.01,1.47,0,2.18-.5,2.18-1.44-.07-.82-.8-.98-2.15-1.3l-.71-.16c-1.76-.48-2.77-.85-2.86-2.56,0-1.77,1.62-2.59,3.28-2.59,2.06,0,3.55.87,3.71,2.91l-1.49.23c-.02-1.21-.82-1.88-2.24-1.88-.89,0-1.77.44-1.77,1.22.09.78.8.98,2.13,1.28l.21.05c.76.16,1.35.32,1.79.48.91.3,1.6.96,1.6,2.22,0,.99-.35,1.7-1.05,2.15-.69.43-1.56.64-2.61.64-2.08,0-3.76-.98-3.76-3.12l1.46-.14h.01Z"/>
+      <path class="cls-1" d="M125.2,113.89h-6.73c.05,1.97.87,2.89,2.52,2.89,1.51,0,2.32-.64,2.54-1.99l1.54.12c-.41,2.06-1.79,3.14-4.06,3.14-1.38,0-2.45-.43-3.19-1.29-.73-.8-1.08-1.93-1.08-3.37,0-1.33.39-2.47,1.12-3.3.78-.87,1.86-1.33,3.14-1.33,1.42,0,2.75.62,3.46,1.76.48.76.76,1.86.76,3,0,.16,0,.28-.02.37ZM118.49,112.59h5.08c-.02-.5-.2-1.17-.48-1.58-.44-.66-1.1-.96-2.08-.96s-1.74.37-2.09.96c-.28.5-.41,1.06-.43,1.58Z"/>
+      <path class="cls-1" d="M127.01,105.43h1.6v1.88h-1.6v-1.88ZM127.01,108.98h1.6v8.87h-1.6v-8.87Z"/>
+      <path class="cls-1" d="M130.94,105.43h1.6v12.42h-1.6v-12.42Z"/>
+      <path class="cls-1" d="M134.88,105.43h1.6v12.42h-1.6v-12.42Z"/>
+      <path class="cls-1" d="M146.77,113.89h-6.73c.05,1.97.87,2.89,2.52,2.89,1.51,0,2.32-.64,2.54-1.99l1.54.12c-.41,2.06-1.79,3.14-4.06,3.14-1.38,0-2.45-.43-3.19-1.29-.73-.8-1.08-1.93-1.08-3.37,0-1.33.39-2.47,1.12-3.3.78-.87,1.86-1.33,3.14-1.33,1.42,0,2.75.62,3.46,1.76.48.76.76,1.86.76,3,0,.16,0,.28-.02.37h0ZM140.06,112.59h5.08c-.02-.5-.2-1.17-.48-1.58-.44-.66-1.1-.96-2.08-.96s-1.74.37-2.09.96c-.28.5-.41,1.06-.43,1.58h0Z"/>
+      <path class="cls-1" d="M196.95,105.43h1.62v8.32c0,1.92,1.46,2.89,3.23,2.89s3.25-.98,3.25-2.89v-8.32h1.61v8.32c0,2.79-1.72,4.31-4.86,4.31s-4.84-1.53-4.84-4.31v-8.32h0Z"/>
+      <path class="cls-1" d="M216.59,117.85h-1.65v-5.18c0-1.06-.02-1.49-.53-2.06-.44-.44-.92-.51-1.58-.51-.59,0-1.12.2-1.6.6-.48.39-.71,1.14-.71,2.25v4.9h-1.6v-8.87h1.6v1.37c.46-1.05,1.37-1.58,2.73-1.58,1.15,0,2,.3,2.64.99.66.76.69,1.61.69,2.82v5.27h.01Z"/>
+      <path class="cls-1" d="M218.84,105.43h1.6v1.88h-1.6v-1.88ZM218.84,108.98h1.6v8.87h-1.6v-8.87Z"/>
+      <path class="cls-1" d="M221.74,108.98h1.7l1.58,4.6c.2.51.48,1.46.89,2.8.32-1.07.62-2.01.91-2.8l1.6-4.6h1.67l-3.32,8.87h-1.7l-3.32-8.87h0Z"/>
+      <path class="cls-1" d="M238.96,113.89h-6.73c.05,1.97.87,2.89,2.52,2.89,1.51,0,2.33-.64,2.54-1.99l1.54.12c-.41,2.06-1.79,3.14-4.06,3.14-1.38,0-2.45-.43-3.19-1.29-.73-.8-1.08-1.93-1.08-3.37,0-1.33.39-2.47,1.12-3.3.78-.87,1.86-1.33,3.14-1.33,1.42,0,2.75.62,3.46,1.76.48.76.76,1.86.76,3,0,.16,0,.28-.02.37h0ZM232.25,112.59h5.08c-.02-.5-.2-1.17-.48-1.58-.44-.66-1.1-.96-2.08-.96s-1.74.37-2.09.96c-.28.5-.41,1.06-.43,1.58h0Z"/>
+      <path class="cls-1" d="M245.69,110.27c-.07-.02-.21-.02-.41-.02-1.81,0-2.91.62-2.91,3.39v4.21h-1.6v-8.87h1.6v1.56c.25-.87,1.35-1.65,2.77-1.76.09-.02.28-.02.59-.02l-.04,1.51Z"/>
+      <path class="cls-1" d="M247.64,114.8c0,1.24.87,2.01,2.27,2.01,1.47,0,2.18-.5,2.18-1.44-.07-.82-.8-.98-2.15-1.3l-.71-.16c-1.76-.48-2.77-.85-2.86-2.56,0-1.77,1.62-2.59,3.28-2.59,2.06,0,3.55.87,3.71,2.91l-1.49.23c-.02-1.21-.82-1.88-2.24-1.88-.89,0-1.78.44-1.78,1.22.09.78.8.98,2.13,1.28l.21.05c.76.16,1.35.32,1.79.48.91.3,1.6.96,1.6,2.22,0,.99-.35,1.7-1.05,2.15-.69.43-1.56.64-2.61.64-2.08,0-3.76-.98-3.76-3.12l1.46-.14h.02Z"/>
+      <path class="cls-1" d="M255.39,105.43h1.6v1.88h-1.6v-1.88h0ZM255.39,108.98h1.6v8.87h-1.6v-8.87h0Z"/>
+      <path class="cls-1" d="M259.82,110.31h-1.28v-1.33h1.28v-2.47h1.58v2.47h1.81v1.33h-1.81v5.5c0,.57.23.69.92.69.21,0,.48-.04.82-.09l.04,1.44c-.39.05-.71.09-.98.09-1.65,0-2.38-.64-2.38-2.08v-5.55Z"/>
+      <path class="cls-1" d="M272.47,113.89h-6.73c.05,1.97.87,2.89,2.52,2.89,1.51,0,2.32-.64,2.54-1.99l1.54.12c-.41,2.06-1.79,3.14-4.06,3.14-1.38,0-2.45-.43-3.19-1.29-.73-.8-1.08-1.93-1.08-3.37,0-1.33.39-2.47,1.12-3.3.78-.87,1.86-1.33,3.14-1.33,1.42,0,2.75.62,3.46,1.76.48.76.76,1.86.76,3,0,.16,0,.28-.02.37h0ZM265.76,112.59h5.08c-.02-.5-.2-1.17-.48-1.58-.44-.66-1.1-.96-2.08-.96s-1.74.37-2.09.96c-.28.5-.41,1.06-.43,1.58ZM268.63,105.42h1.79l-1.63,2.25h-1.31l1.15-2.25Z"/>
+    </g>
+  </g>
+</svg>

docs/presentations/autre/WinterSchoolGDRCyber2026/images/logo_dalgo.svg

@@ -0,0 +1,128 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="71pt" height="19pt" viewBox="0 0 71 19" version="1.1">
+<defs>
+<g>
+<symbol overflow="visible" id="glyph0-0">
+<path style="stroke:none;" d="M 0.75 0 L 4.46875 0 L 4.46875 -5.3125 L 0.75 -5.3125 Z M 4.078125 -4.90625 L 4.078125 -0.703125 L 1.375 -4.90625 Z M 1.140625 -4.59375 L 3.84375 -0.390625 L 1.140625 -0.390625 Z M 1.140625 -4.59375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-1">
+<path style="stroke:none;" d="M 1.3125 0 L 1.3125 -3.875 L 0.640625 -3.875 L 0.640625 0 Z M 1.3125 -4.5 L 1.3125 -5.46875 L 0.640625 -5.46875 L 0.640625 -4.5 Z M 1.3125 -4.5 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-2">
+<path style="stroke:none;" d="M 3.046875 -1.046875 C 3.046875 -1.8125 2.96875 -1.953125 1.84375 -2.234375 C 1.1875 -2.390625 1.1875 -2.46875 1.1875 -2.90625 C 1.1875 -3.25 1.265625 -3.390625 1.84375 -3.390625 C 2.15625 -3.390625 2.59375 -3.34375 2.921875 -3.28125 L 2.96875 -3.828125 C 2.640625 -3.90625 2.234375 -3.953125 1.859375 -3.953125 C 0.84375 -3.953125 0.53125 -3.640625 0.53125 -2.921875 C 0.53125 -2.109375 0.609375 -1.90625 1.578125 -1.671875 C 2.359375 -1.484375 2.390625 -1.4375 2.390625 -1.015625 C 2.390625 -0.609375 2.28125 -0.5 1.671875 -0.5 C 1.34375 -0.5 0.90625 -0.5625 0.5625 -0.65625 L 0.484375 -0.125 C 0.78125 -0.015625 1.3125 0.078125 1.71875 0.078125 C 2.828125 0.078125 3.046875 -0.28125 3.046875 -1.046875 Z M 3.046875 -1.046875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-3">
+<path style="stroke:none;" d="M 2.578125 -0.578125 C 2.328125 -0.515625 2.140625 -0.484375 1.953125 -0.484375 C 1.59375 -0.484375 1.546875 -0.625 1.546875 -0.921875 L 1.546875 -3.328125 L 2.59375 -3.328125 L 2.65625 -3.875 L 1.546875 -3.875 L 1.546875 -4.9375 L 0.890625 -4.84375 L 0.890625 -3.875 L 0.203125 -3.875 L 0.203125 -3.328125 L 0.890625 -3.328125 L 0.890625 -0.8125 C 0.890625 -0.15625 1.1875 0.078125 1.84375 0.078125 C 2.140625 0.078125 2.421875 0.03125 2.65625 -0.0625 Z M 2.578125 -0.578125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-4">
+<path style="stroke:none;" d="M 2.328125 -3.953125 C 1.9375 -3.796875 1.546875 -3.5625 1.265625 -3.34375 L 1.21875 -3.875 L 0.640625 -3.875 L 0.640625 0 L 1.3125 0 L 1.3125 -2.671875 C 1.625 -2.90625 2.046875 -3.171875 2.421875 -3.34375 Z M 2.328125 -3.953125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-5">
+<path style="stroke:none;" d="M 3.671875 -2.75 C 3.671875 -3.484375 3.34375 -3.953125 2.53125 -3.953125 C 2.046875 -3.953125 1.578125 -3.828125 1.3125 -3.6875 L 1.3125 -5.5625 L 0.640625 -5.46875 L 0.640625 -0.078125 C 1.078125 0.03125 1.671875 0.078125 2.03125 0.078125 C 3.359375 0.078125 3.671875 -0.484375 3.671875 -1.375 Z M 1.3125 -3.078125 C 1.5625 -3.203125 2.03125 -3.375 2.375 -3.375 C 2.828125 -3.375 3 -3.171875 3 -2.765625 L 3 -1.34375 C 3 -0.828125 2.859375 -0.515625 2.078125 -0.515625 C 1.828125 -0.515625 1.5625 -0.53125 1.3125 -0.5625 Z M 1.3125 -3.078125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-6">
+<path style="stroke:none;" d="M 0.59375 -3.875 L 0.59375 -0.90625 C 0.59375 -0.3125 0.828125 0.078125 1.4375 0.078125 C 1.90625 0.078125 2.578125 -0.125 3 -0.328125 L 3.0625 0 L 3.609375 0 L 3.609375 -3.875 L 2.9375 -3.875 L 2.9375 -0.953125 C 2.53125 -0.734375 1.921875 -0.5625 1.640625 -0.5625 C 1.390625 -0.5625 1.265625 -0.65625 1.265625 -0.921875 L 1.265625 -3.875 Z M 0.59375 -3.875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-7">
+<path style="stroke:none;" d="M 1.109375 -1.359375 L 1.109375 -1.6875 L 3.421875 -1.6875 L 3.421875 -2.5 C 3.421875 -3.296875 3.109375 -3.953125 1.953125 -3.953125 C 0.8125 -3.953125 0.4375 -3.3125 0.4375 -2.515625 L 0.4375 -1.34375 C 0.4375 -0.46875 0.828125 0.078125 1.96875 0.078125 C 2.46875 0.078125 2.984375 -0.015625 3.34375 -0.140625 L 3.265625 -0.671875 C 2.84375 -0.5625 2.421875 -0.5 2.03125 -0.5 C 1.28125 -0.5 1.109375 -0.734375 1.109375 -1.359375 Z M 1.109375 -2.5625 C 1.109375 -3.09375 1.328125 -3.40625 1.953125 -3.40625 C 2.59375 -3.40625 2.765625 -3.09375 2.765625 -2.5625 L 2.765625 -2.234375 L 1.109375 -2.234375 Z M 1.109375 -2.5625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-8">
+<path style="stroke:none;" d="M 0.5 -1.109375 C 0.5 -0.328125 0.859375 0.078125 1.625 0.078125 C 2.140625 0.078125 2.59375 -0.09375 2.90625 -0.34375 L 2.96875 0 L 3.53125 0 L 3.53125 -5.5625 L 2.859375 -5.46875 L 2.859375 -3.84375 C 2.546875 -3.90625 2.09375 -3.953125 1.75 -3.953125 C 0.84375 -3.953125 0.5 -3.46875 0.5 -2.6875 Z M 2.859375 -0.96875 C 2.578125 -0.71875 2.140625 -0.515625 1.765625 -0.515625 C 1.296875 -0.515625 1.15625 -0.703125 1.15625 -1.109375 L 1.15625 -2.6875 C 1.15625 -3.15625 1.34375 -3.375 1.796875 -3.375 C 2.0625 -3.375 2.5 -3.328125 2.859375 -3.25 Z M 2.859375 -0.96875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph1-0">
+<path style="stroke:none;" d="M 1.359375 0 L 8.046875 0 L 8.046875 -9.546875 L 1.359375 -9.546875 Z M 7.34375 -8.828125 L 7.34375 -1.28125 L 2.46875 -8.828125 Z M 2.0625 -8.265625 L 6.921875 -0.703125 L 2.0625 -0.703125 Z M 2.0625 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph1-1">
+<path style="stroke:none;" d="M 5.296875 -9.546875 L 3.625 -9.546875 L 0.40625 0 L 1.65625 0 L 2.421875 -2.296875 L 6.484375 -2.296875 L 7.265625 0 L 8.515625 0 Z M 6.171875 -3.375 L 2.75 -3.375 L 4.453125 -8.65625 Z M 6.171875 -3.375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph1-2">
+<path style="stroke:none;" d="M 2.453125 -9.546875 L 1.21875 -9.546875 L 1.21875 0 L 6.59375 0 L 6.59375 -1.109375 L 2.453125 -1.109375 Z M 2.453125 -9.546875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph1-3">
+<path style="stroke:none;" d="M 2.234375 -6.8125 C 2.234375 -8.109375 2.71875 -8.578125 4.28125 -8.578125 C 5.078125 -8.578125 5.9375 -8.484375 6.859375 -8.328125 L 7 -9.390625 C 6.109375 -9.59375 5.15625 -9.703125 4.34375 -9.703125 C 1.96875 -9.703125 1 -8.8125 1 -6.875 L 1 -2.671875 C 1 -0.90625 1.75 0.140625 4.1875 0.140625 C 5.171875 0.140625 6.28125 0 7.21875 -0.265625 L 7.21875 -4.390625 L 6.03125 -4.390625 L 6.03125 -1.140625 C 5.359375 -1.015625 4.734375 -0.96875 4.234375 -0.96875 C 2.59375 -0.96875 2.234375 -1.515625 2.234375 -2.734375 Z M 2.234375 -6.8125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph1-4">
+<path style="stroke:none;" d="M 7.921875 -6.796875 C 7.921875 -8.390625 6.921875 -9.703125 4.453125 -9.703125 C 2 -9.703125 1 -8.390625 1 -6.796875 L 1 -2.75 C 1 -1.15625 2 0.140625 4.453125 0.140625 C 6.921875 0.140625 7.921875 -1.15625 7.921875 -2.75 Z M 2.234375 -6.765625 C 2.234375 -7.953125 2.953125 -8.609375 4.453125 -8.609375 C 5.96875 -8.609375 6.6875 -7.953125 6.6875 -6.765625 L 6.6875 -2.78125 C 6.6875 -1.609375 5.96875 -0.953125 4.453125 -0.953125 C 2.953125 -0.953125 2.234375 -1.609375 2.234375 -2.78125 Z M 2.234375 -6.765625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph2-0">
+<path style="stroke:none;" d="M 0.75 0 L 4.46875 0 L 4.46875 -5.3125 L 0.75 -5.3125 Z M 4.078125 -4.90625 L 4.078125 -0.703125 L 1.375 -4.90625 Z M 1.140625 -4.59375 L 3.84375 -0.390625 L 1.140625 -0.390625 Z M 1.140625 -4.59375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph2-1">
+<path style="stroke:none;" d="M 2.328125 -3.953125 C 1.9375 -3.796875 1.546875 -3.5625 1.265625 -3.34375 L 1.21875 -3.875 L 0.640625 -3.875 L 0.640625 0 L 1.3125 0 L 1.3125 -2.671875 C 1.625 -2.90625 2.046875 -3.171875 2.421875 -3.34375 Z M 2.328125 -3.953125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph2-2">
+<path style="stroke:none;" d="M 1.3125 0 L 1.3125 -3.875 L 0.640625 -3.875 L 0.640625 0 Z M 1.3125 -4.5 L 1.3125 -5.46875 L 0.640625 -5.46875 L 0.640625 -4.5 Z M 1.3125 -4.5 "/>
+</symbol>
+<symbol overflow="visible" id="glyph2-3">
+<path style="stroke:none;" d="M 2.578125 -0.578125 C 2.328125 -0.515625 2.140625 -0.484375 1.953125 -0.484375 C 1.59375 -0.484375 1.546875 -0.625 1.546875 -0.921875 L 1.546875 -3.328125 L 2.59375 -3.328125 L 2.65625 -3.875 L 1.546875 -3.875 L 1.546875 -4.9375 L 0.890625 -4.84375 L 0.890625 -3.875 L 0.203125 -3.875 L 0.203125 -3.328125 L 0.890625 -3.328125 L 0.890625 -0.8125 C 0.890625 -0.15625 1.1875 0.078125 1.84375 0.078125 C 2.140625 0.078125 2.421875 0.03125 2.65625 -0.0625 Z M 2.578125 -0.578125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph2-4">
+<path style="stroke:none;" d="M 3.65625 0 L 3.65625 -2.96875 C 3.65625 -3.5625 3.421875 -3.953125 2.8125 -3.953125 C 2.34375 -3.953125 1.734375 -3.765625 1.3125 -3.546875 L 1.3125 -5.5625 L 0.640625 -5.46875 L 0.640625 0 L 1.3125 0 L 1.3125 -2.921875 C 1.71875 -3.140625 2.3125 -3.328125 2.609375 -3.328125 C 2.859375 -3.328125 2.984375 -3.21875 2.984375 -2.96875 L 2.984375 0 Z M 3.65625 0 "/>
+</symbol>
+<symbol overflow="visible" id="glyph2-5">
+<path style="stroke:none;" d="M 6 0 L 6 -2.96875 C 6 -3.5625 5.765625 -3.953125 5.140625 -3.953125 C 4.65625 -3.953125 4.015625 -3.765625 3.546875 -3.546875 C 3.4375 -3.8125 3.203125 -3.953125 2.8125 -3.953125 C 2.34375 -3.953125 1.671875 -3.75 1.25 -3.546875 L 1.171875 -3.875 L 0.640625 -3.875 L 0.640625 0 L 1.3125 0 L 1.3125 -2.9375 C 1.71875 -3.140625 2.3125 -3.328125 2.609375 -3.328125 C 2.859375 -3.328125 2.984375 -3.21875 2.984375 -2.96875 L 2.984375 0 L 3.65625 0 L 3.65625 -2.9375 C 4.0625 -3.140625 4.625 -3.328125 4.953125 -3.328125 C 5.203125 -3.328125 5.328125 -3.21875 5.328125 -2.96875 L 5.328125 0 Z M 6 0 "/>
+</symbol>
+<symbol overflow="visible" id="glyph2-6">
+<path style="stroke:none;" d="M 3.046875 -1.046875 C 3.046875 -1.8125 2.96875 -1.953125 1.84375 -2.234375 C 1.1875 -2.390625 1.1875 -2.46875 1.1875 -2.90625 C 1.1875 -3.25 1.265625 -3.390625 1.84375 -3.390625 C 2.15625 -3.390625 2.59375 -3.34375 2.921875 -3.28125 L 2.96875 -3.828125 C 2.640625 -3.90625 2.234375 -3.953125 1.859375 -3.953125 C 0.84375 -3.953125 0.53125 -3.640625 0.53125 -2.921875 C 0.53125 -2.109375 0.609375 -1.90625 1.578125 -1.671875 C 2.359375 -1.484375 2.390625 -1.4375 2.390625 -1.015625 C 2.390625 -0.609375 2.28125 -0.5 1.671875 -0.5 C 1.34375 -0.5 0.90625 -0.5625 0.5625 -0.65625 L 0.484375 -0.125 C 0.78125 -0.015625 1.3125 0.078125 1.71875 0.078125 C 2.828125 0.078125 3.046875 -0.28125 3.046875 -1.046875 Z M 3.046875 -1.046875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph3-0">
+<path style="stroke:none;" d="M 2.359375 0 L 13.90625 0 L 13.90625 -16.5 L 2.359375 -16.5 Z M 12.6875 -15.265625 L 12.6875 -2.203125 L 4.265625 -15.265625 Z M 3.5625 -14.28125 L 11.96875 -1.21875 L 3.5625 -1.21875 Z M 3.5625 -14.28125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph3-1">
+<path style="stroke:none;" d="M 2.109375 -16.5 L 2.109375 0 L 7.875 0 C 11.921875 0 13.1875 -2.109375 13.1875 -4.734375 L 13.1875 -11.765625 C 13.1875 -14.390625 11.921875 -16.5 7.875 -16.5 Z M 4.234375 -14.59375 L 7.8125 -14.59375 C 10.3125 -14.59375 11.046875 -13.5625 11.046875 -11.625 L 11.046875 -4.875 C 11.046875 -2.953125 10.3125 -1.90625 7.8125 -1.90625 L 4.234375 -1.90625 Z M 4.234375 -14.59375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph4-0">
+<path style="stroke:none;" d="M 0.75 0 L 4.46875 0 L 4.46875 -5.3125 L 0.75 -5.3125 Z M 4.078125 -4.90625 L 4.078125 -0.703125 L 1.375 -4.90625 Z M 1.140625 -4.59375 L 3.84375 -0.390625 L 1.140625 -0.390625 Z M 1.140625 -4.59375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph4-1">
+<path style="stroke:none;" d="M 2.578125 -0.578125 C 2.328125 -0.515625 2.140625 -0.484375 1.953125 -0.484375 C 1.59375 -0.484375 1.546875 -0.625 1.546875 -0.921875 L 1.546875 -3.328125 L 2.59375 -3.328125 L 2.65625 -3.875 L 1.546875 -3.875 L 1.546875 -4.9375 L 0.890625 -4.84375 L 0.890625 -3.875 L 0.203125 -3.875 L 0.203125 -3.328125 L 0.890625 -3.328125 L 0.890625 -0.8125 C 0.890625 -0.15625 1.1875 0.078125 1.84375 0.078125 C 2.140625 0.078125 2.421875 0.03125 2.65625 -0.0625 Z M 2.578125 -0.578125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph4-2">
+<path style="stroke:none;" d="M 1.109375 -1.359375 L 1.109375 -1.6875 L 3.421875 -1.6875 L 3.421875 -2.5 C 3.421875 -3.296875 3.109375 -3.953125 1.953125 -3.953125 C 0.8125 -3.953125 0.4375 -3.3125 0.4375 -2.515625 L 0.4375 -1.34375 C 0.4375 -0.46875 0.828125 0.078125 1.96875 0.078125 C 2.46875 0.078125 2.984375 -0.015625 3.34375 -0.140625 L 3.265625 -0.671875 C 2.84375 -0.5625 2.421875 -0.5 2.03125 -0.5 C 1.28125 -0.5 1.109375 -0.734375 1.109375 -1.359375 Z M 1.109375 -2.5625 C 1.109375 -3.09375 1.328125 -3.40625 1.953125 -3.40625 C 2.59375 -3.40625 2.765625 -3.09375 2.765625 -2.5625 L 2.765625 -2.234375 L 1.109375 -2.234375 Z M 1.109375 -2.5625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph4-3">
+<path style="stroke:none;" d="M 3.390625 -2.703125 C 3.390625 -3.53125 3.015625 -3.953125 1.90625 -3.953125 C 1.5 -3.953125 1 -3.890625 0.640625 -3.796875 L 0.703125 -3.265625 C 1.015625 -3.328125 1.5 -3.390625 1.875 -3.390625 C 2.5 -3.390625 2.71875 -3.21875 2.71875 -2.734375 L 2.71875 -2.125 L 1.6875 -2.125 C 0.90625 -2.125 0.5 -1.84375 0.5 -1.03125 C 0.5 -0.34375 0.796875 0.078125 1.515625 0.078125 C 1.984375 0.078125 2.4375 -0.046875 2.78125 -0.28125 L 2.828125 0 L 3.390625 0 Z M 2.71875 -0.8125 C 2.421875 -0.625 2.046875 -0.5 1.71875 -0.5 C 1.234375 -0.5 1.15625 -0.65625 1.15625 -1.046875 C 1.15625 -1.4375 1.3125 -1.5625 1.734375 -1.5625 L 2.71875 -1.5625 Z M 2.71875 -0.8125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph4-4">
+<path style="stroke:none;" d="M 6 0 L 6 -2.96875 C 6 -3.5625 5.765625 -3.953125 5.140625 -3.953125 C 4.65625 -3.953125 4.015625 -3.765625 3.546875 -3.546875 C 3.4375 -3.8125 3.203125 -3.953125 2.8125 -3.953125 C 2.34375 -3.953125 1.671875 -3.75 1.25 -3.546875 L 1.171875 -3.875 L 0.640625 -3.875 L 0.640625 0 L 1.3125 0 L 1.3125 -2.9375 C 1.71875 -3.140625 2.3125 -3.328125 2.609375 -3.328125 C 2.859375 -3.328125 2.984375 -3.21875 2.984375 -2.96875 L 2.984375 0 L 3.65625 0 L 3.65625 -2.9375 C 4.0625 -3.140625 4.625 -3.328125 4.953125 -3.328125 C 5.203125 -3.328125 5.328125 -3.21875 5.328125 -2.96875 L 5.328125 0 Z M 6 0 "/>
+</symbol>
+</g>
+</defs>
+<g id="surface425">
+<g style="fill:rgb(100%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-1" x="15.8132" y="7.6061"/>
+  <use xlink:href="#glyph0-2" x="17.757904" y="7.6061"/>
+  <use xlink:href="#glyph0-3" x="21.256778" y="7.6061"/>
+  <use xlink:href="#glyph0-4" x="24.197745" y="7.6061"/>
+  <use xlink:href="#glyph0-1" x="26.652536" y="7.6061"/>
+  <use xlink:href="#glyph0-5" x="28.59724" y="7.6061"/>
+  <use xlink:href="#glyph0-6" x="32.733722" y="7.6061"/>
+  <use xlink:href="#glyph0-3" x="36.981786" y="7.6061"/>
+  <use xlink:href="#glyph0-7" x="39.922752" y="7.6061"/>
+  <use xlink:href="#glyph0-8" x="43.756371" y="7.6061"/>
+</g>
+<g style="fill:rgb(0%,0%,100%);fill-opacity:1;">
+  <use xlink:href="#glyph1-1" x="14.9753" y="17.8972"/>
+  <use xlink:href="#glyph1-2" x="23.898636" y="17.8972"/>
+  <use xlink:href="#glyph1-3" x="30.856543" y="17.8972"/>
+  <use xlink:href="#glyph1-4" x="39.148647" y="17.8972"/>
+</g>
+<g style="fill:rgb(0%,0%,100%);fill-opacity:1;">
+  <use xlink:href="#glyph2-1" x="47.41309" y="17.9683"/>
+  <use xlink:href="#glyph2-2" x="49.867881" y="17.9683"/>
+  <use xlink:href="#glyph2-3" x="51.812585" y="17.9683"/>
+  <use xlink:href="#glyph2-4" x="54.753552" y="17.9683"/>
+  <use xlink:href="#glyph2-5" x="59.001615" y="17.9683"/>
+  <use xlink:href="#glyph2-6" x="65.592888" y="17.9683"/>
+</g>
+<g style="fill:rgb(100%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph3-1" x="1.0542" y="18.4178"/>
+</g>
+<g style="fill:rgb(62.7%,12.5%,94.1%);fill-opacity:1;">
+  <use xlink:href="#glyph4-1" x="50.36293" y="9.6069"/>
+  <use xlink:href="#glyph4-2" x="53.303897" y="9.6069"/>
+  <use xlink:href="#glyph4-3" x="57.121575" y="9.6069"/>
+  <use xlink:href="#glyph4-4" x="61.050834" y="9.6069"/>
+</g>
+</g>
+</svg>

docs/presentations/autre/WinterSchoolGDRCyber2026/localiteetat_hc.tex

@@ -0,0 +1,34 @@
+\resizebox{\columnwidth}{!}{%
+    \begin{tikzpicture}[
+        roundnode/.style={circle, draw=black, fill=black, very thick, minimum size=1pt,},
+        ignorednode/.style={circle, draw=black!20, fill=black!20, very thick, minimum size=1pt,},
+        arrow/.style={|->, thick,},
+        message/.style={->, blue!50, dashed, -{Circle[length=4pt,]}},
+        ]
+
+        \node[roundnode, draw=red, fill=red] (11) {};
+        \node[left] at (11.west) {$p_0$};
+        \node[above] at (11.north) {$w(1)$};
+        \node[roundnode, draw=blue, fill=blue] (12) [right=of 11] {};
+        \node[above] at (12.north) {$r/(0,0)$};
+        \node[roundnode, draw=blue, fill=blue] (13) [right=of 12] {};
+        \node[above] at (13.north) {$r/(0,2)^w$};
+
+        \draw[arrow] (11) -- (12);
+        \draw[arrow] (12) -- (13);
+
+        \node[roundnode, draw=blue, fill=blue] (21) [below=of 11] {};
+        \node[left] at (21.west) {$p_1$};
+        \node[below] at (21.south) {$w(2)$};
+        \node[roundnode, draw=red, fill=red] (22) [right=of 21] {};
+        \node[below] at (22.south) {$r/(0,0)$};
+        \node[roundnode, draw=red, fill=red] (23) [right=of 22] {};
+        \node[below] at (23.south) {$r/(0,1)^w$};
+
+        \draw[arrow] (21) -- (22);
+        \draw[arrow] (22) -- (23);
+
+        \draw[message] (11) -- ($(22)!0.5!(23)$);
+        \draw[message] (21) -- ($(12)!0.5!(13)$);
+    \end{tikzpicture}
+}

docs/presentations/autre/WinterSchoolGDRCyber2026/main.tex

@@ -0,0 +1,265 @@
+\documentclass{beamer}
+\usetheme{Boadilla}
+\usecolortheme{orchid}
+
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage[french]{babel}
+\usepackage{stackengine}
+
+\addtobeamertemplate{navigation symbols}{}{%
+    \usebeamerfont{footline}%
+    \usebeamercolor[fg]{footline}%
+    \hspace{1em}%
+    \insertframenumber/\inserttotalframenumber
+}
+\usepackage{ulem}
+\usepackage{tkz-tab}
+\setbeamertemplate{blocks}[rounded]%
+[shadow=true]
+\AtBeginSection{%
+    \begin{frame}
+        \tableofcontents[sections=\value{section}]
+    \end{frame}
+}
+
+\usepackage{tikz}
+\usetikzlibrary{positioning}
+\usetikzlibrary{calc}
+\usetikzlibrary{arrows.meta}
+
+\title{Amaury JOLY - Winter School GDR Cybersécurité}
+\author{Amaury JOLY}
+\institute{Université Aix-Marseille \\ Laboratoire d'Informatique et Systèmes (LIS)}
+\date{Janvier 2026}
+
+\begin{document}
+
+\begin{frame}
+    \titlepage 
+    \vspace{-1.2em}
+
+    \begin{center}
+      \includegraphics[height=1cm]{images/logoamu}\hspace{1cm}%
+      \includegraphics[height=1.5cm]{images/logolis}\hspace{1cm}
+      \includegraphics[height=0.9cm]{images/logodalgo}\hspace{1cm}%
+      \includegraphics[height=0.6cm]{images/logoparsec}
+    \end{center}
+\end{frame}
+
+
+\begin{frame}{Who am I?}
+  \begin{itemize}
+    \item \textbf{Amaury JOLY}
+    \item 3rd-year PhD candidate at the \textbf{Laboratory of Informatics and Systems (LIS)}
+    \item \textbf{Distributed Algorithms} team
+    \item Supervised by \textbf{Emmanuel GODARD} and \textbf{Corentin TRAVERS}
+    \item \textbf{CIFRE} PhD with the company \textbf{Parsec}
+  \end{itemize}
+\end{frame}
+
+%------------------------------------------------------------
+\begin{frame}{Parsec: company \& product}
+  \begin{itemize}
+    \item \textbf{Parsec} develops an end-to-end encrypted file sharing platform
+    \item Client--server solution: users collaborate through shared workspaces
+    \item \textbf{End-to-end encryption}: the server only sees \emph{ciphertexts}
+    \item \textbf{Distributed PKI management among clients} (keys/identities handled at the edge)
+    \item \alert{one central server stores encrypted data and redistributes it to clients}
+  \end{itemize}
+\end{frame}
+
+%------------------------------------------------------------
+\begin{frame}{My topic (high level)}
+  \begin{block}{Problem statement}
+    \textit{``Weak consistency in a zero-trust cloud for real-time collaborative applications.''}
+  \end{block}
+
+  \vspace{0.4em}
+  \begin{itemize}
+    \item Real-time collaboration: concurrent updates, low latency, intermittent connectivity
+    \item We want \textbf{weak consistency} (e.g., eventual / causal behaviors) with clear semantics under concurrency
+    \item \textbf{Zero-trust cloud} (Parsec-like setting):
+      \begin{itemize}
+        \item central server trusted for \textbf{availability} only
+        \item server can be \textbf{honest-but-curious} (observes metadata, stores/forwards ciphertexts)
+        \item \textbf{no trust assumptions on clients} (they may be compromised or mutually distrustful)
+      \end{itemize}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+    \frametitle{Our Model}
+        \begin{block}{Assumptions}
+            \begin{itemize}
+                \item The system is highly connected
+                \item The system is not partitionable
+                \item The system is asynchronous (i.e., no assumption on message delays or relative process speeds)
+                \item Nodes can fail by \textbf{crash} (i.e., stop functioning)
+                \item Nodes can be \textbf{Byzantine} (i.e., arbitrary behavior)
+                \item The communication network is reliable but byzantine nodes can delay or reorder messages
+                \item There is a Reliable Broadcast abstraction available
+            \end{itemize}
+        \end{block}
+\end{frame}
+
+\begin{frame}
+    \frametitle{Consistency classes}
+    \begin{columns}
+        \column{0.5\textwidth}
+        \resizebox{\columnwidth}{!}{
+            \includegraphics{images/carte_criteres.png}
+        }
+
+        \column{0.5\textwidth}
+        One approach to define the consistency of an algorithm is to place the concurrent history it produces into a consistency class. \\
+        We can define 3 consistency classes:
+        \begin{itemize}
+            \item \textbf{State Locality} (LS)
+            \item \textbf{Validity} (V)
+            \item \textbf{Eventual Consistency} (EC)
+        \end{itemize}
+    \end{columns}
+\end{frame}
+
+\begin{frame}
+    \frametitle{State Locality (LS)}
+
+    \begin{columns}
+        \column{0.4\textwidth}
+        \include{localiteetat_hc}
+        \column{0.6\textwidth}
+        \begin{block}{Definition}
+            For every process $p$, there exists a linearization containing all of $p$'s read operations. \\
+        \end{block}
+        \begin{math}
+            \begin{array}{ll}
+                e.g.: & \textcolor{blue}{C_{p_1} = \{r/(0,0), r/(0,2)^w, w(2)\}}, \\
+                      & \textcolor{red}{C_{p_2} = \{r/(0,0), r/(0,1)^w, w(1)\}},  \\
+                      & \textcolor{blue}{r/(0,0) \bullet w(2) \bullet r/(0,2)^w}  \\
+                      & \textcolor{red}{r/(0,0) \bullet w(1) \bullet r/(0,1)^w}   \\
+            \end{array}
+        \end{math}
+    \end{columns}
+
+
+    \begin{flushright}
+        \begin{math}
+            LS = \left\{
+            \begin{array}{l}
+                \mathcal{T} \rightarrow \mathcal{P}(\mathcal{H}) \\
+                T \rightarrow \left\{
+                \begin{tabular}{lll}
+                    $H \in \mathcal{H}:$ & \multicolumn{2}{l}{$\forall p \in \mathcal{P}_H, \exists C_p \subset E_H,$}                                                       \\
+                                         &                                                                             & $\hat{Q}_{T,H} \subset C_p$                         \\
+                                         & $\land$                                                                     & $lin(H[p \cap C_p / C_p]) \cap L(T) \neq \emptyset$ \\
+                \end{tabular}
+                \right.                                          \\
+            \end{array}
+            \right.
+        \end{math}
+    \end{flushright}
+\end{frame}
+
+
+\begin{frame}
+    \frametitle{Validity (V)}
+
+    \begin{columns}
+        \column{0.4\textwidth}
+        \include{validite_hc}
+        \column{0.6\textwidth}
+        \begin{block}{Definition}
+            There exists a co-finite set of events such that for each of them, a linearization of all write operations justifies them. \\
+        \end{block}
+        \begin{math}
+            \begin{array}{ll}
+                e.g.: & E' = \{r/(2,1)^w, r/(1,2)^w\}                        \\
+                      & w(2) \bullet w(1) \bullet \textcolor{red}{r/(2,1)^w} \\
+                      & w(1) \bullet w(2) \bullet \textcolor{red}{r/(1,2)^w} \\
+            \end{array}
+        \end{math}
+    \end{columns}
+
+
+    \begin{flushright}
+        \begin{math}
+            V = \left\{
+            \begin{array}{l}
+                \mathcal{T} \rightarrow \mathcal{P}(\mathcal{H}) \\
+                T \rightarrow \left\{
+                \begin{array}{lll}
+                    H \in \mathcal{H}: & \multicolumn{2}{l}{|U_{T,H}| = \infty}                                                                       \\
+                                       & \lor                                   & \exists E' \subset E_H, (|E_H \setminus E'| < \infty                \\
+                                       &                                        & \land \forall e \in E', lin(H[E_H / {e}]) \cap L(T) \neq \emptyset) \\
+                \end{array}
+                \right.                                          \\
+            \end{array}
+            \right.
+        \end{math}
+    \end{flushright}
+\end{frame}
+
+
+\begin{frame}
+    \frametitle{Eventual Consistency (EC)}
+
+    \begin{columns}
+        \column{0.4\textwidth}
+        \include{convergence_hc}%
+        \column{0.5\textwidth}
+        \begin{block}{Definition}
+            There exists a co-finite set of events such that for each of them, a single linearization justifies them. \\
+        \end{block}
+        \begin{math}
+            \begin{array}{ll}
+                e.g.: & E' = \{r/(1,2)^w, r/(1,2)^w\}                        \\
+                      & w(1) \bullet w(2) \bullet \textcolor{red}{r/(1,2)^w} \\
+            \end{array}
+        \end{math}
+    \end{columns}
+
+
+    \begin{flushright}
+        \begin{math}
+            EC = \left\{
+            \begin{array}{l}
+                \mathcal{T} \rightarrow \mathcal{P}(\mathcal{H}) \\
+                T \rightarrow \left\{
+                \begin{array}{lll}
+                    H \in \mathcal{H}: & \multicolumn{2}{l}{|U_{T,H}| = \infty}                                                                                  \\
+                                       & \lor                                   & \exists E' \subset E_H, |E_H \setminus E'| < \infty                            \\
+                                       &                                        & \land \displaystyle\bigcap_{e \in E'} \delta_T^{-1}(\lambda(e)) \neq \emptyset \\
+                \end{array}
+                \right.                                          \\
+            \end{array}
+            \right.
+        \end{math}
+    \end{flushright}
+\end{frame}
+
+\begin{frame}{Main Work}
+    \begin{itemize}
+        \item We designed a distributed algorithm that use a \textbf{byzantine-tolerant eventually consistent register} in our model to achieve Agreement with $t < n/3$ Byzantine nodes.
+        \item I'm working on a framework using this algorithm to build collaborative applications for the context of a zero-trust cloud. 
+    \end{itemize}
+\end{frame}
+
+\begin{frame}
+    \frametitle{Thank you for your attention!}
+    \vfill
+    \begin{center}
+        \includegraphics[height=1cm]{images/logoamu}\hspace{1cm}%
+        \vspace{1em}
+
+        \includegraphics[height=1.5cm]{images/logolis}\hspace{1cm}%
+        \vspace{1em}
+
+        \includegraphics[height=0.9cm]{images/logodalgo}\hspace{1cm}%
+        \vspace{1em}
+
+        \includegraphics[height=0.6cm]{images/logoparsec}
+    \end{center}
+\end{frame}
+
+\end{document}

docs/presentations/autre/WinterSchoolGDRCyber2026/validite_hc.tex

@@ -0,0 +1,31 @@
+\resizebox{\columnwidth}{!}{%
+    \begin{tikzpicture}[
+        roundnode/.style={circle, draw=black, fill=black, very thick, minimum size=1pt,},
+        ignorednode/.style={circle, draw=black!20, fill=black!20, very thick, minimum size=1pt,},
+        arrow/.style={|->, thick,},
+        message/.style={->, blue!50, dashed, -{Circle[length=4pt,]}},
+        ]
+
+        \node[roundnode] (11) {};
+        \node[left] at (11.west) {$p_0$};
+        \node[above] at (11.north) {$w(1)$};
+        \node[roundnode] (12) [right=of 11] {};
+        \node[above] at (12.north) {$r/(0,1)$};
+        \node[roundnode] (13) [right=of 12] {};
+        \node[above] at (13.north) {$r/(2,1)^w$};
+
+        \draw[arrow] (11) -- (12);
+        \draw[arrow] (12) -- (13);
+
+        \node[roundnode] (21) [below=of 11] {};
+        \node[left] at (21.west) {$p_1$};
+        \node[below] at (21.south) {$w(2)$};
+        \node[roundnode] (22) [right=of 21] {};
+        \node[below] at (22.south) {$r/(0,2)$};
+        \node[roundnode] (23) [right=of 22] {};
+        \node[below] at (23.south) {$r/(1,2)^w$};
+
+        \draw[arrow] (21) -- (22);
+        \draw[arrow] (22) -- (23);
+    \end{tikzpicture}
+}