fix du devcontainer

.devcontainer/devcontainer.json

@@ -6,7 +6,7 @@
     "containerEnv": { //Add your build arguments here
         "DEBIAN_FRONTEND": "noninteractive"
     },
-    "runArgs": ["--net=host"], //Add you docker run arguments here
+    // "runArgs": ["--net=host"], //Add you docker run arguments here
     "updateContentCommand": ".devcontainer/install-tools.sh", //Path to the installation script run inside the DevContainer
     // "customizations": {
     //     //Add your customizations here

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,34 @@
+\subsection{Reliable Broadcast (RB)}
+
+\RB provides the following properties in the model.
+\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}
+
+\subsection{DenyList Object}
+
+ We assume a linearizable DenyList (\DL) object as in~\cite{frey:disc23} with the following properties.
+  
+    The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
+    \begin{itemize}
+      \item \textbf{Termination.} A $\PROVE$, an $\APPEND$, or a $\READ$ operation invoked by a correct process always returns.
+      \item \textbf{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if:
+      \begin{itemize}
+        \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,6 @@
+
+Processes export \ABbroadcast$(m)$ and $m = \ABdeliver()$. \ARB requires 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*}
+plus Integrity/No-duplicates/Validity (inherited from \RB and the construction).

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

@@ -0,0 +1,455 @@
+We present below an example of implementation of Atomic Reliable Broadcast (\ARB) using a Reliable Broadcast (\RB) primitive and a DenyList (\DL) object according to the model and notations defined in Section 2.
+
+\subsection{Algorithm}
+% granularité diff commentaire de code et paragraphe pre algo
+
+\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}
+
+\subsubsection{Variables}
+Each process $p_i$ maintains:
+
+\LinesNotNumbered
+\begin{algorithm}
+  $\received \gets \emptyset$\; %\Comment{Messages received via \RB but not yet delivered}
+  $\delivered \gets \emptyset$\; %\Comment{Messages already delivered}
+  $\prop[r][j] \gets \bot,\ \forall r,j$\; %\Comment{Proposal from process $j$ for round $r$}
+  $\current \gets 0$\;
+\end{algorithm}
+
+% \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}
+
+\LinesNumbered
+\begin{algorithm}[H]
+  \caption{\RB handler (at process $p_i$)}\label{alg:rb-handler}
+  \Fn{RBreceived($S, r, j$)}{
+    $\received \leftarrow \received \cup \{S\}$\;\nllabel{code:receivedConstruction}
+    $\prop[r][j] \leftarrow S$\;\nllabel{code:prop-set} % \Comment{Record sender $j$'s proposal $S$ for round $r$}
+  }
+\end{algorithm}
+
+% \paragraph{} An \ABbroadcast$(m)$ chooses the next open round from the \DL view, proposes all pending messages together with the new $m$, disseminates this proposal via \RB, then executes $\PROVE(r)$ followed by $\APPEND(r)$ to freeze the winners of the round. The loop polls \DL until (i) some winner’s proposal includes $m$ in a \emph{closed} round and (ii) all winners' proposals for closed rounds are known locally, ensuring eventual inclusion and delivery.
+
+\begin{algorithm}[H]\label{alg:ABroadcast}
+  \caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast}
+    \Fn{ABbroadcast($m$)}{
+      $P \leftarrow \READ()$\;\nllabel{code:set-up-read} %\Comment{Fetch latest \DL state to learn recent $\PROVE$ operations}
+      $r_{max} \leftarrow \max(\{ r' : \exists j,\ (j,r') \in P \})$\;\nllabel{code:rmax-compute} %\Comment{Pick current open round}
+      $S \leftarrow (\received \setminus \delivered) \cup \{m\}$\;\nllabel{code:Sconstruction} 
+      %\Comment{Propose all pending messages plus the new $m$}
+
+      \vspace{1em}
+
+      $r \gets r_{max} - 1$\;
+      \While{$((i, r) \not\in P\ \wedge (\nexists j, r': (j, r') \in P \wedge m \in \prop[r'][j]))$}{\nllabel{code:sumbited-check-loop}
+        $r \gets r + 1$\;\nllabel{code:round-increment}
+        $\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$;\;\nllabel{code:submit-proposition}
+        $P \leftarrow \READ()$\; % \Comment{Refresh local view of \DL}
+      }
+    }
+\end{algorithm}
+
+\begin{algorithm}[H]\label{alg:ADeliver}
+  \caption{\ABdeliver() at process $p_i$}\label{alg:delivery}
+    \Fn{ABdeliver($\bot$)}{
+      $r \gets \current$\;
+      $P_r \gets \{(j,r): (j,r) \in \READ()\}$ \;
+      \If{$P_r = \emptyset$}{\nllabel{code:check-if-winners}
+        \Return{$\bot$}
+      }
+      $\APPEND(r)$; $P \gets \READ()$\; \nllabel{code:append-read}
+      $W_r \gets \{ j : (j, \PROVEtrace(r)) \in P \}$\;\nllabel{code:Wcompute}
+      \If{$\exists j \in W_r,\ \prop[r][j] = \bot$}{ \nllabel{code:check-winners-ack}
+        \Return{$\bot$}
+      }
+      $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$\;\nllabel{code:Mcompute}
+      $m \gets \ordered(M_r \setminus \delivered)[0]$\;\nllabel{code:next-msg-extraction}
+       %\Comment{Set $m$ as the smaller message not already delivered}
+      $\delivered \leftarrow \delivered \cup \{m\}$\;
+      \If{$M_r \setminus \delivered = \emptyset$}{ %\Comment{Check if all messages from round $r$ have been delivered}
+        $\current \leftarrow \current + 1$
+      }
+      \Return{$m$}
+    }
+\end{algorithm}
+
+% ------------------------------------------------------------------------------
+\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, hence the lemma is true.
+
+  \emph{Induction.} Assume the lemma is true for round $r\geq 0$, we prove it for round $r+1$.
+  
+  \smallskip
+  Assume $r+1$ is closed and by \cref{def:first-append} $\APPEND^{(\star)}(r+1)$ be the earliest $\APPEND(r+1)$ in the DL linearization $H$.
+  By Lemma 1, after an $\APPEND(r)$ were in $H$, any later $\PROVE(r)$ will be invalid also, a process’s program order is preserved in $H$.
+  
+  There are two possibilities for where $\APPEND^{(\star)}(r+1)$ is invoked.
+
+  \begin{itemize}
+    \item \textbf{Case Algorithm \ref{alg:ABroadcast} :}
+    Some process executes the loop at \ref{code:sumbited-check-loop} and invokes $\PROVE(r+1);\APPEND^{(\star)}(r+1)$ at line~\ref{code:submit-proposition}. Let $p_i$ be this process.
+    Immediately before line~\ref{code:submit-proposition}, line~\ref{code:round-increment} sets $r\leftarrow r+1$, so the previous loop iteration targeted $r$. We consider two sub-cases.
+    
+    \begin{itemize}
+      \item \emph{(i) $p_i$ is not in its first loop iteration.}
+      In the previous iteration, $p_i$ executed $\PROVE_i(r)$ at \ref{code:submit-proposition}, followed (in program order) by $\APPEND_i(r)$. 
+      If round $r$ wasn't closed when $p_i$ execute $\PROVE_i(r)$ at \ref{code:submit-proposition}, then the condition at \ref{code:sumbited-check-loop} would be true hence the tuple $(i, r)$ should be visible in P which implies that $p_i$ should leave the loop at round $r$, contradicting the assumption that $p_i$ is now executing another iteration.
+      Since the tuple is not visible, the $\PROVE_i(r)$ was invalid which implies by definition that an $\APPEND(r)$ already exists in $H$. Thus in this case $r$ is closed.
+    
+      \item \emph{(ii) $p_i$ is in its first loop iteration.}
+      To compute the value $r_{max}$, $p_i$ must have observed one or many $(\_ , r+1)$ in $P$ at \ref{code:rmax-compute}, issued by some processes (possibly different from $p_i$). Let's call $p_j$ the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$. \\
+      When $p_j$ executed $P \gets \READ()$ at \ref{code:set-up-read} and compute $r_{max}$ at \ref{code:rmax-compute}, he observed no tuple $(\_,r+1)$ in $P$ because he's the issuer of the first one. So when $p_j$ executed the loop (\ref{code:sumbited-check-loop}), he run it for the round $r$, didn't seen any $(j,r)$ in $P$ at B6, and then executed the first $\PROVE_j(r+1)$ at \ref{code:submit-proposition} in a second iteration. \\
+      If round $r$ wasn't closed when $p_j$ execute $\PROVE_j(r)$ at \ref{code:submit-proposition}, then the $(j, r)$ will be in $P$ and the condition at \ref{code:sumbited-check-loop} should be true which implies that $p_j$ sould leave the loop at round $r$, contradicting the assumption that $p_j$ is now executing $\PROVE_j(r+1)$. In this case $r$ is closed.
+    \end{itemize}
+    
+    \item \textbf{Case Algorithm \ref{alg:ADeliver} :} 
+    Some process invokes $\APPEND(r+1)$ at \ref{code:append-read}. Let $p_i$ be this process.  
+    Line~\ref{code:append-read} is guarded by the condition at \ref{code:check-if-winners}, which ensures that $p_i$ observed some $(\_,r+1)$ in $P$. Let $p_j$ be the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$.
+    When $p_j$ executed $\PROVE_j(r+1)$ at \ref{code:submit-proposition}, he observed no tuple $(\_,r+1)$ in $P$ at \ref{code:check-if-winners} because he's the issuer of the first one. By the same reasoning as in the Case Algorithm \ref{alg:ABroadcast} (ii), $p_j$ must have observed that the round $r$ was closed. 
+    % Line C7 is guarded by the presence of $\PROVE(r)$ in $P$ with $r=r+1$ (C5). 
+    % Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C17), so if a process can reach $\textit{next}=r+1$ it implies that he has completed round $r$, which includes closing $r$ at C8 when $\PROVE(r)$ is observed. 
+    % Hence $\APPEND^\star(r+1)$ implies a prior $\APPEND(r)$ in $H$, so $r$ is closed.
+  \end{itemize}
+  
+  \smallskip
+  In all cases, $r+1$ closed implies $r$ closed. By induction on $r$, if the lemma is true for a closed $r$ then it is true for a closed $r+1$.
+  Therefore, the lemma is true for all closed rounds $r$.
+\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 $(\_,\PROVEtrace(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 $(\_,\PROVEtrace(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 $W_r$ at line~\ref{code:Wcompute}, then :
+  \begin{itemize}
+    \item $\Winners_r$ is defined;
+    \item the computed $W_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 $W_r$. \\
+  By program order, $p_i$ must have executed $\APPEND_i(r)$ at line~\ref{code:append-read} 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 $(\_,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:append-read} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\_,r)$ such that
+  \[
+    W_r = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
+  \]
+\end{proof}
+
+\begin{lemma}[No APPEND without PROVE]\label{lem:append-prove}
+If some process invokes $\APPEND(r)$, then at least a process must have previously invoked $\PROVE(r)$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Consider the round $r$ such that some process invokes $\APPEND(r)$. There are two possible cases
+  
+  \begin{itemize}
+    \item \textbf{Case (\ref{code:submit-proposition}) :}
+    There exists a process $p_i$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p_i$ must have previously invoked $\PROVE_i(r)$ before invoking $\APPEND^{(\star)}(r)$ at line~\ref{code:submit-proposition}. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by a correct process before $\APPEND^{(\star)}(r)$.
+    
+    \item \textbf{Case (\ref{code:append-read}) :}
+    There exists a process $p_i$ that invoked $\APPEND^{(\star)}(r)$ at . Line~\ref{code:append-read} is guarded by the condition at \ref{code:check-if-winners}, which ensures that $p$ observed some $(\_,r)$ in $P$. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by some process before $\APPEND^{(\star)}(r)$.
+  \end{itemize}
+    
+  In both cases, if some process invokes $\APPEND(r)$, then some process must have previously invoked $\PROVE(r)$.
+\end{proof}
+
+\begin{lemma}[No empty winners]\label{lem:nonempty}
+  Let $r$ be a closed round, then $\Winners_r \neq \emptyset$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the DL linearization. \\
+  By \Cref{lem:append-prove}, at least one process must have invoked a valid $\PROVE(r)$ before $\APPEND^{(\star)}(r)$. Hence, there exists at least one $p_j$ such that $p_j$ invoked $\PROVE_j(r) \prec \APPEND^\star(r)$, so $\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 invoked a $\RBcast(S^{(i)}, r, i)$ and hence any correct will eventually 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 exist a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $i$ invoked a valid $\PROVE_i(r)$ at line~\ref{code:submit-proposition} he must have invoked $\RBcast(S^{(i)}, r, i)$ directly before.
+
+  Let take a correct process $p_j$, by \RB \emph{Validity}, every correct process eventually receives $i$'s \RB message for round $r$, which sets $\prop[r][i]$ to a non-$\bot$ value at line~\ref{code:prop-set}.
+\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_r$ at line~\ref{code:Mcompute}, 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_r$ at line~\ref{code:Mcompute}. 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} where $p_i$ computes $M_r$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, $M_r = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]$, we have $\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$ invokes at most one $\RBcast(S, r, i)$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  By program order, any process $p_i$ invokes $\RBcast(S, r, i)$ at line~\ref{code:submit-proposition} must be in the loop \ref{code:sumbited-check-loop}. No matter the number of iterations of the loop, line~\ref{code:sumbited-check-loop} always uses the current value of $r$ which is incremented by 1 at each turn. Hence, in any execution, any process $p_i$ invokes $\RBcast(S, r, j)$ at most once for any 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}, we have
+  \[
+    M_r^{(i)} = \Messages_r
+  \]
+\end{lemma}
+
+\begin{proof}[Proof]
+  Let take a correct process $p_i$ that compute $M_r$ at line~\ref{code:Mcompute}. That implies that $p_i$ has defined $W_r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $W_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$ invokes at most one $\RBcast(S^{(j)}, r, j)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes
+  \[
+    M_r^{(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$ invokes
+  \[
+  \RBcast(S, r, j)\quad\text{for same S with}\quad m\in S.
+  \]
+\end{lemma}
+
+\begin{proof}
+  Fix a correct process $p_i$ that invokes $\ABbroadcast(m)$ and eventually exits the loop (\ref{code:sumbited-check-loop}) at some round $r$. There are two possible cases.
+
+  \begin{itemize}
+    \item \textbf{Case 1:} $p_i$ exits the loop because $(i, r) \in P$. In this case, by \Cref{def:winner-invariant}, $p_i$ is a winner in round $r$. By program order, $p_i$ must have invoked $\RBcast(S, r, i)$ at \ref{code:submit-proposition} before invoking $\PROVE_i(r)$. By line~\ref{code:Sconstruction}, $m \in S$. Hence there exist a closed round $r$ and $p_i$ is a correct process such that $i\in\Winners_r$. Hence, $i$ invokes $\RBcast(S, r, i)$ with $m\in S$.
+    
+    \item \textbf{Case 2:} $p_i$ exits the loop because $\exists j, r': (j, r') \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:winners-propose} and \Cref{lem:unique-proposal} $p_j$ must have invoked a unique $\RBcast(S, r', j)$. Which set $\prop^{(i)}[r'][j] = S$ with $m \in S$.
+  \end{itemize}
+    
+  In both cases, if some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a correct process $j\in\Winners_r$ such that $j$ invokes
+  \[
+    \RBcast(S, r, j)\quad\text{with}\quad m\in S.
+  \]
+\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]
+  Consider a correct process $p_i$ that invokes $\ABbroadcast(m)$. The statement is true if $\exists r_1$ such that $r_1 \geq r_{max}$ and if $(i, r_1) \in P$; or if $\exists r_2$ such that $r_2 \geq r_{max}$ and if $\exists j: (j, r_2) \in P \wedge m \in \prop[r_2][j]$ (like guarded at B8).
+
+  Consider that there exists no round $r_1$ such that $p_i$ invokes a valid $\PROVE(r_1)$. In this case $p_i$ invokes infinitely many $\RBcast(S, \_, i)$ at line~\ref{code:submit-proposition} with $m \in S$ (line~\ref{code:Sconstruction}).\\
+  The assumption that no $\PROVE(r_1)$ invoked by $p$ is valid implies by \DL \emph{Validity} that for every round $r' \geq r_{max}$, there exists at least one $\APPEND(r')$ in the DL linearization, hence by \Cref{lem:nonempty} for every possible round $r'$ there at least a winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least one process $p_k$ that invokes infinitely many valid $\PROVE(r')$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $p_k$ eventually receives $p_i$ 's \RB messages. Let call $t_0$ the time when $p_k$ receives $p_i$ 's \RB message. \\
+  At $t_0$, $p_k$ executes Algorithm \ref{alg:rb-handler} and sets $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line~\ref{code:receivedConstruction}). 
+  For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \texttt{RReceived()}, $p_k$ must include $m$ in his proposal $S$ at line~\ref{code:Sconstruction} (because $m$ is pending in $j$'s $\received \setminus \delivered$ set). There exists a minimum round $r_2$ such that $p_k \in \Winners_{r_2}$ after $t_0$. By \Cref{lem:winners-propose}, eventually $\prop^{(i)}[r_2][k] \neq \bot$. By \Cref{lem:unique-proposal}, $\prop^{(i)}[r_2][k]$ is uniquely defined as the set $S$ proposed by $p_k$ at B6, which by \Cref{lem:inclusion} includes $m$. Hence eventually $m \in \prop^{(i)}[r_2][k]$ and $k \in \Winners_{r_2}$. 
+
+  So if $p_i$ is a winner he satisfies the condition $(i, r_1) \in P$. And we show that if the first condition is never satisfied, the second one will eventually be satisfied. Hence either the first or the second condition will eventually be satisfied, and $p_i$ eventually exits the loop and returns from $\ABbroadcast(m)$.
+\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$ invokes
+  \[
+    \RBcast(S, r, j)\quad\text{with}\quad m\in S.
+  \]
+
+  By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line~\ref{code:Mcompute}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(S, r, j)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes
+  \[
+    M_r = \bigcup_{k\in\Winners_r} \prop[r][k],
+  \]
+  we have $m \in \prop[r][j] = S$, so $m \in M_r$. By \Cref{lem:convergence}, $M_r$ is invariant so each computation of $M_r$ by a correct process includes $m$. At each invocation of $m' = \ABdeliver()$, $m'$ is added to $\delivered$ until $M_r \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 C18 to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reached line~\ref{code:next-msg-extraction} to extract the next message to deliver, it can't be $m$ because $m \not\in (M_r \setminus \{..., m, ...\})$. 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 a 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
+  \[
+    \RBcast(S_1, r'_1, k_1)\quad\text{with}\quad m_1\in S_1,
+  \]
+  \[
+    \RBcast(S_2, r'_2, k_2)\quad\text{with}\quad m_2\in S_2.
+  \]
+
+  Let consider three 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_{r_1}$ (which contains $m_1$) to increment $\current$ and eventually set $\current = r_2$ to compute $M_{r_2}$ 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_{r_1}$ at line~\ref{code:Mcompute} 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{lemma}[Fifo Order]\label{lem:fifo-order}
+  For any two distints messages $m_1$ and $m_2$ broadcast by the same correct process $p_i$, if $p_i$ invokes $\ABbroadcast(m_1)$ before $\ABbroadcast(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}
+  Let take $m_1$ and $m_2$ broadcast by the same correct process $p_i$, with $p_i$ invoking $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$. By \Cref{lem:validity}, there exist closed rounds $r_1$ and $r_2$ such that $r_1 \leq r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that
+  \[
+    \RBcast(S_1, r_1, k_1)\quad\text{with}\quad m_1\in S_1,
+  \]
+  \[
+    \RBcast(S_2, r_2, k_2)\quad\text{with}\quad m_2\in S_2.
+  \]
+
+  By program order, $p_i$ must have invoked $\RBcast(S_1, r_1, i)$ before $\RBcast(S_2, r_2, i)$. By \Cref{lem:unique-proposal}, any process invokes at most one $\RBcast(S, r, i)$ per round, hence $r_1 < r_2$. By \Cref{lem:total-order}, any correct process that delivers both $m_1$ and $m_2$ delivers them in a deterministic order.
+  
+  In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
+\end{proof}
+
+\begin{theorem}[FIFO-\ARB]
+Under the assumed $\DL$ synchrony and $\RB$ reliability, the algorithm implements FIFO Atomic Reliable Broadcast.
+\end{theorem}
+
+\begin{proof}
+  We show that the algorithm satisfies the properties of FIFO Atomic Reliable Broadcast under the assumed $\DL$ synchrony and $\RB$ reliability.
+
+  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 the underlying $\RB$ primitive.
+  By the Integrity property of $\RB$, every such message was previously $\RBcast$ by some process, 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.
+  Furthermore, \Cref{lem:fifo-order} states that for any two messages $m_1$ and $m_2$ broadcast by the same correct process, any correct process that delivers both messages delivers $m_1$ before $m_2$ whenever $m_1$ was broadcast before $m_2$.
+  Thus the global total order extends the per-sender FIFO order of $\ABbroadcast$.
+
+  All the above lemmas are proved under the assumptions that $\DL$ satisfies the required synchrony properties and that the underlying primitive is a Reliable Broadcast ($\RB$) with Integrity, No-duplicates and Validity.
+  Therefore, under these assumptions, the algorithm satisfies Validity, Integrity/No-duplicates, total order and per-sender FIFO order, and hence implements FIFO 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 upgrade a Reliable Broadcast ($\RB$) primitive into FIFO Atomic Reliable Broadcast ($\ARB$). 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
+such as described in 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 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}

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

@@ -0,0 +1,428 @@
+
+\subsection{Model extension}
+We consider a static set $\Pi$ of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable. At most $f$ processes may be Byzantine, and we assume $n > 3f$.
+
+\paragraph{Synchrony.} The network is asynchronous.
+
+\paragraph{Communication.} Processes can exchange through a Reliable Broadcast ($\RB$) primitive (defined below) which is invoked with the functions $\RBcast(m)$ and $m = \RBreceived()$. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$.
+
+\paragraph{Byzantine behaviour}
+A process is said to exhibit Byzantine behaviour if it deviates arbitrarily from the prescribed algorithm. Such deviations may, for instance, consist in invoking primitives ($\RBcast$, $\APPEND$, $\PROVE$, etc.) with invalid inputs or inputs crafted maliciously, colluding with other Byzantine processes in an attempt to manipulate the system state or violate its guarantees, deliberately delaying or accelerating the delivery of messages to selected nodes so as to disrupt the expected timing of operations, or withholding messages and responses in order to induce inconsistencies in the system state.
+
+Byzantine processes are constrained by the following. They cannot forge valid cryptographic signatures or threshold shares without access to the corresponding private keys. They cannot violate the termination, validity, or anti-flickering properties of the $\DL$ object. They also cannot break the integrity, no-duplicates, or validity properties of the $\RB$ primitive.
+
+
+\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}
+
+\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, \PROVEtrace(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}
+
+\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]
+    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, \PROVEtrace(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]
+    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}
+
+\subsubsection{Variables}
+Each process $p_i$ maintains the following local variables:
+\LinesNotNumbered
+\begin{algorithm}
+    $\texttt{last\_commited} \gets 0$\;
+    $\texttt{last\_delivered} \gets 0$\;
+    $\received \gets \emptyset$\;
+    $\delivered \gets \emptyset$\;
+    $\prop[r][j] \gets \bot, \forall r, j$\;
+    $W[r] \gets \bot, \forall r$; this is the set of the winners for the round $r$\\
+    $B[r] \gets \bot, \forall r$; this is the set of processes who have bahaved maliciously for round $r$\\
+    $\resolved[r] \gets \bot, \forall r$\;
+    $Y$ a $\BFTDL$ such that the value space is $\mathcal{R} \times \Pi$\;
+    $V$ a $\BFTDL$ such that the value space is $(\mathcal{R} \times \mathcal{M} \times \Pi)$\;
+\end{algorithm}
+
+\LinesNumbered
+\begin{algorithm}[H]
+    \caption{$\ABbroadcast(m)$ at process $p_i$}\label{alg:broadcast-bft}
+    \SetAlgoLined
+    \Fn{ABroadcast($m$)}{
+        $\received \gets \received \cup \{m\}$\;
+        Propose()\;
+    }
+\end{algorithm}
+
+
+\begin{algorithm}[H]
+    \caption{Propose($\bot$) at process $p_i$}\label{alg:propose-bft}
+    \SetAlgoLined
+    % \Statex \textbf{Proposer Job}
+    \Fn{Propose($\bot$)}{
+        $r \gets \texttt{last\_commited}$\;
+        \While{$S \neq \emptyset$ with $S \gets \received \setminus (\delivered \cup (\bigcup_{r' < r} \bigcup_{\substack{(j,S')\in W[r']\\ j\notin B[r']\\ S' \in \prop[r'][j]}} S'))$}{
+            % \Comment{PROP PHASE}\;
+            \tcc*[f]{PROP PHASE}\\
+            $V.\BFTPROVE((r, S, i))$\;
+            $\RBcast(i, \texttt{PROP}, S, r)$\;
+            \textbf{wait} until $|\{j: \exists S, |\{k: (k,(r, S, j)) \in V.\BFTREAD()\}| \geq t+1\}| \geq n - t$\;
+            % \Comment{COMMIT PHASE}
+            \tcc*[f]{COMMIT PHASE}\\
+            \For{\textbf{each} $j \in \Pi$}{
+                % $Y[j].\BFTAPPEND(r)$\;
+                $V.\BFTAPPEND((r, S, j))$\;
+                $Y.\BFTAPPEND((r, j))$\;
+            }
+            $\RBcast(i, \texttt{COMMIT}, r)$\;
+            \textbf{wait} until $|\resolved[r]| \geq n - t$\;
+            % \Comment*{X PHASE}
+            % \tcc*[f]{X PHASE}\\
+            \BlankLine
+            $W[r] \gets \{(j, S): |\{k: (k, (r, S, j)) \in V.\BFTREAD()\}| \geq t+1\}$\;
+            $B[r] \gets \{j: |\{k: (k, (r, j)) \in Y.\BFTREAD()\}| \geq t+1\}$\;
+            $r \gets r + 1$\;
+        }
+        $\texttt{last\_commited} \gets r$\;
+    }
+\end{algorithm}
+
+\begin{algorithm}[H]
+    \caption{$\ABdeliver()$ at process $p_i$}\label{alg:deliver-bft}
+    \SetAlgoLined
+    \Fn{ADeliver($\bot$)}{
+        $r \gets \texttt{last\_delivered}$\;
+        \If{$|\resolved[r]| < n - t$}{
+            \Return{$\bot$}
+        }
+        $W \gets \{(j, S): |\{k: (k, (r, S, j)) \in V.\BFTREAD()\}| \geq t+1\}$\;
+        $B \gets \{j: |\{k: (k, (r, j)) \in Y.\BFTREAD()\}| \geq t+1\}$\;
+
+        \If{$\exists (j, S) \in W, j \notin B, S \notin \prop[r][j]$}{
+            \Return{$\bot$}
+        }
+        \BlankLine
+        $M \gets \bigcup_{\substack{(j,S)\in W\\ j\notin B\\ S \in prop[r][j]}} S$\;\nllabel{code:Mcompute}
+        $m \gets \ordered(M \setminus \delivered)[0]$\;
+        % \Comment*{Set $m$ as the smaller message not already delivered}
+        $\delivered \leftarrow \delivered \cup \{m\}$\;
+        \If{$M \setminus \delivered = \emptyset$}{
+            $\texttt{last\_delivered} \gets \texttt{last\_delivered} + 1$\;
+        }
+        % \Comment*{Check if all messages from round $r$ have been delivered}
+        \Return{$m$}
+    }
+\end{algorithm}
+
+\begin{algorithm}[H]
+    \caption{RB handler at process $p_i$}\label{alg:rb-handler-bft}
+    \SetAlgoLined
+    \Upon{$Rdeliver(j, \texttt{PROP}, S, r)$}{
+        $\received \gets \received \cup \{S\}$\;
+        \uIf{$\prop[r][j] = \bot \vee (\{S' : (j, (r, S', j)) \in V.\BFTREAD()\} = \{S\})$}{
+            $V.\BFTPROVE((r, S, j))$\;
+        }
+        \Else{
+            $Y.\BFTPROVE((r, j))$\;
+        }
+        $\prop[r][j] \gets \prop[r][j] \cup S$\;
+        Propose()\;
+    }
+
+    \vspace{1em}
+
+    \Upon{$Rdeliver(j, \texttt{COMMIT}, r)$}{
+        $\resolved[r] \gets \resolved[r] \cup \{j\}$\;
+    }
+\end{algorithm}
+
+\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}
+
+\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}
+}

misc/InstalParty2026/main.tex

@@ -0,0 +1,291 @@
+\documentclass[aspectratio=43,10pt]{beamer}
+
+\usetheme{Madrid}
+\usecolortheme{default}
+\usefonttheme{professionalfonts}
+\setbeamertemplate{navigation symbols}{}
+
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage[french]{babel}
+\usepackage{lmodern}
+\usepackage{microtype}
+
+\usepackage{tikz}
+\usetikzlibrary{positioning,fit,calc,arrows.meta}
+
+\title{}
+\subtitle{}
+\author{}
+\institute{}
+\date{}
+
+\begin{document}
+
+\begin{frame}{Install Party Linux}
+  \framesubtitle{Luminy - 18 fevrier 2026}
+  \centering
+      \includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/logo-6011e.png}
+\end{frame}
+
+\begin{frame}{Architecture d'un système d'exploitation}
+
+  Un OS c'est :
+  \begin{itemize}
+    \item Un Noyau (Kernel) : Ordonnancement, gestion de la mémoire, intéraction entre les composants physiques.
+    \item Des Bibliothèques (Drivers) : UN driver est UNE interface avec un composant physique. (Carte Graphique, carte réseau, imprimante, \dots)
+    \item Une Interface Graphique : Comment sont agenceés et gérées les fenetres
+    \item Des Application : Les logiciels à utiliser
+  \end{itemize}
+
+\end{frame}
+
+\begin{frame}{Architecture d'un système d'exploitation}
+
+  Un OS c'est :
+
+  \vspace{1em}
+
+  \centering
+  \begin{tikzpicture}[
+    box/.style={draw, rounded corners, align=center, minimum width=6cm, minimum height=0.9cm},
+    arrow/.style={-{Latex[length=3mm,width=2mm]}, thick}
+  ]
+    \pause
+    \node[box] at (0, 5) (Noyau) {Noyau \\ (XNU, Windows NT, Linux, BSD, \dots)};
+    \pause
+    \node[box] at (0, 4) (Drivers) {Drivers \\ (Carte Graphique, disques durs, carte réseau, \dots)};
+    \node[box, red] at (0, 3) (Drivers) {Materiel};
+    \pause
+    \node[box] at (0, 6) (GUI) {GUI \\ (DWM, Quartz Compositor + WindowServer, X11 + Gnome, Wayland + Swayne)};
+    \pause
+    \node[box] at (0, 7) (Apps) {Applications};
+  \end{tikzpicture}
+
+\end{frame}
+
+\begin{frame}{Architecture d'un système d'exploitation}
+  
+  Dans le cas de Windows, une version de windows = un package Noyau/GUI/Drivers définit et immuable + quelques applications par defaut
+
+  \vspace{1em}
+
+  \centering
+  \begin{tikzpicture}[
+    box/.style={draw, rounded corners, align=center, minimum width=6cm, minimum height=0.9cm},
+    arrow/.style={-{Latex[length=3mm,width=2mm]}, thick}
+  ]
+    \node[box] at (0, 5) (Noyau) {Noyau \\ Windows NT};
+    \node[box] at (0, 4) (Drivers) {Drivers};
+    \node[box] at (0, 3) (Drivers) {Materiel};
+    \node[box] at (0, 6) (GUI) {GUI \\ DWM};
+    \node[box] at (0, 7) (Apps) {Applications \\ Microsoft Edge, Outlook, Skype, \dots};
+  \end{tikzpicture}
+
+  \pause
+
+  \textcolor{red}{Une distribution Linux c'est pareil !} \\
+  \pause
+  Une distribution = un package Noyau/GUI/Drivers définit + quelques applications par defaut
+
+\end{frame}
+
+\begin{frame}{Allons un peu plus en détail - L'interface graphique}
+
+  D'un point de vue de "à quoi ca ressemble", une distribution linux peut jouer sur 3 facteurs :
+  \begin{itemize}
+    \item Le serveur d'affichage (Xorg ou Weston principalement)
+    \item Le gestionnaire de fenetres (flottant ou tiling)
+    \item L'interface graphique (Gnome, KDE)
+  \end{itemize}
+  
+  \begin{center}
+  \resizebox{0.8\width}{!}{
+    \begin{tikzpicture}[
+      box/.style={draw, rounded corners, align=center, minimum width=6cm, minimum height=0.9cm},
+      arrow/.style={-{Latex[length=3mm,width=2mm]}, thick}
+    ]
+      \node[box] at (0, 5) (Noyau) {Noyau \\ Linux};
+      \node[box] at (0, 4) (Drivers) {Drivers};
+      \node[box] at (0, 3) (Drivers) {Materiel};
+      \node[box] at (0, 6) (GUI) {Serveur d'affichage \\ Xorg, Weston};
+      \node[box] at (6, 6) (GUI) {Windows Manager \\ Compiz, KWin, Awesome, I3};
+      \node[box] at (0, 7) (GUI) {Interface Graphique \\ Gnome, KDE};
+      \node[box] at (0, 8) (Apps) {Applications};
+    \end{tikzpicture}
+    }
+  \end{center}
+
+\end{frame}
+
+\begin{frame}{Allons un peu plus en détail - L'interface graphique}
+
+  
+  
+  \begin{center}
+    \begin{minipage}{0.49\textwidth}
+    \centering
+    \includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/canonical.png}
+    \par\smallskip
+    \small GNOME
+    \end{minipage}
+    \hfill
+    \begin{minipage}{0.49\textwidth}
+    \centering
+    \includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/xfce.jpg}
+    \par\smallskip
+    \small Xfce
+    \end{minipage}
+
+    \vspace{4mm}
+
+    \begin{minipage}{0.49\textwidth}
+    \centering
+    \includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/plasma.png}
+    \par\smallskip
+    \small KDE Plasma
+    \end{minipage}
+    \hfill
+    \begin{minipage}{0.49\textwidth}
+    \centering
+    \includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/i3.png}
+    \par\smallskip
+    \small i3 (tiling)
+    \end{minipage}
+  \end{center}
+
+\end{frame}
+
+\begin{frame}{Allons un peu plus en détail - La gestion des paquets}
+  Pour installer une applications sous windows :
+  \pause
+  \begin{itemize}
+    \item On execute un installeur (.msi ou .exe)
+    \item On execute une version "portable" (.exe)
+  \end{itemize}
+  \pause
+  \vspace{1em}
+  Sous linux c'est pareil :
+  \begin{itemize}
+    \item On execute un installeur (.dnf ou .deb)
+    \item On execute une version portable (Snap, Appimage, Flatpak, \dots)
+  \end{itemize}
+
+  \pause
+  \vspace{1em}
+  Le support des format d'installer dependent des distribution. \\
+  Les version portable (ou conteneurisé) sont a priori universel.
+\end{frame}
+
+\begin{frame}{Allons un peu plus en détail - La gestion des paquets}
+  On distingue donc deux grandes familles (en vrai y'en a plus que ca) \\
+  RPM Package Manager et dpkg.
+
+  \pause
+
+  \begin{center}
+    \begin{tikzpicture}[
+      font=\small,
+      n/.style={draw, rounded corners, align=center, minimum height=8mm, inner sep=3pt},
+      a/.style={-{Latex[length=3mm,width=2mm]}, thick},
+      node distance=10mm and 14mm
+    ]
+
+    \node[n] (rpm) {RPM\\DNF};
+    \node[n, below=5mm of rpm] (dpkg) {DPKG\\APT};
+
+    \node[n, right=10mm of rpm] (redhat) {Red Hat};
+    \node[n, right=10mm of redhat] (fedora) {Fedora};
+    \node[n, right=10mm of fedora] (nobara) {Nobara};
+
+    \node[n, right=10mm of dpkg] (debian) {Debian};
+    \node[n, right=10mm of debian] (ubuntu) {Ubuntu};
+    \node[n, right=10mm of ubuntu] (mint) {Linux Mint};
+
+    \draw[a] (rpm) -- (redhat);
+    \draw[a] (redhat) -- (fedora);
+    \draw[a] (fedora) -- (nobara);
+
+    \draw[a] (dpkg) -- (debian);
+    \draw[a] (debian) -- (ubuntu);
+    \draw[a] (ubuntu) -- (mint);
+
+    \pause
+    \node[n, below=5mm of dpkg] (tar) {tar.xx \\ PacMan};
+
+    \node[n, right=10mm of tar] (arch) {Arch Linux};
+    \node[n, right=10mm of arch] (manjaro) {Manjaro};
+
+    \draw[a] (tar) -- (arch);
+    \draw[a] (arch) -- (manjaro);
+
+    \end{tikzpicture}
+  \end{center}
+
+\end{frame}
+
+\begin{frame}{Allons un peu plus en détail - La gestion des paquets}
+  Les grosses différences de chaque gestionnaire sont plutot philosophique :
+  \begin{itemize}
+    \pause
+    \item APT : Image de stabilité et de grand publique. 
+    \begin{itemize}
+      \item + : Très stable, grosse communauté donc beaucoup de ressources dont en francais.
+      \item - : Souvent plus en retard sur des versions très recentes de certains logiciels.
+    \end{itemize}
+    \pause
+
+    \item DNF : Image de robustesse avec une image plus d'usage professionel
+    \begin{itemize}
+      \item + : Très robuste, moins de chance de casser le système même pour des configurations exotiques
+      \item - : Le processus de mise à jour peut être plus lent, et plus compliqué à prendre en main que APT.
+    \end{itemize}
+    \pause
+
+    \item PacMan : Minimaliste et ultra à jour.
+    \begin{itemize}
+      \item + : Systeme de "Rolling Release" qui permet d'avoir les mise à jour en continu.
+      \item - : Necessite un plus grand travail de veille sur les mise à jour.
+    \end{itemize}
+  \end{itemize}
+
+\end{frame}
+
+\begin{frame}{Quelques autres trucs à savoir}
+  \begin{itemize}
+    \item /bin (binaries): Exécutables essentiels au système, utilisables par tous les utilisateurs
+    \pause
+    \item /boot: fichiers permettant à Linux de démarrer
+    \pause
+    \item /dev (device): Fichiers spéciaux représentant les point d'entrées de tous les périphériques (fichiers spéciaux des disques durs, écrans, partitions, consoles TTY, webcam, clavier, ...)
+    \pause
+    \item /etc (editing text config): Contient les fichiers de configuration du système et des setvices (*.conf, passwd, inittab, fstab)
+    \pause
+    \item /home: Répertoire personnel des utilisateurs
+    \pause
+    \item /mnt (mount) /media: Là où les ressources peuvent être montées de manière permanente (/media) ou temporaire (/mnt)
+    \pause
+    \item /root: Répertoire personnel du super utilisateur
+    \pause
+    \item /sbin (super binaries): Contient les programmes système essentiels utilisables par l'admin uniquement.
+    \pause
+    \item /tmp (temporary): Répertoire fichier temporaires
+    \pause
+    \item /usr (Unix System Resources): Contient des programmes, des librairies et des données utilisés par tous les utilisateurs du système
+    \pause
+    \item /var (variable): contient les données variables qui varient en fonction de l'utilisation du système. (logs, bdd, mails)
+  \end{itemize}
+\end{frame}
+
+\begin{frame}{Comment ca s'installe}
+  \begin{itemize}
+    \item Faire un backup
+    \item Avoir une clé usb bootable
+    \item Rentrer dans la selection du disque de boot en trouvant le bon FX
+    \item Tester en execution "live" que tout fonctionne bien
+    \item Choisir si on veut du mono ou dual-boot
+    \item Allouer ses partitions en fonction des ses usages
+  \end{itemize}
+\end{frame}
+
+\end{document}