\documentclass[11pt]{article}

\usepackage[margin=1in]{geometry}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{thmtools}
\usepackage{enumitem}
\usepackage{csquotes}
\usepackage[hidelinks]{hyperref}
\usepackage[nameinlink,noabbrev]{cleveref}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{graphicx}
% Line-number prefix configuration (A/B/C)
\renewcommand{\thealgorithm}{\Alph{algorithm}} % Float labels: Algorithm A, B, C
\newcommand{\algletter}{}
\algrenewcommand\alglinenumber[1]{\scriptsize\textbf{\algletter}#1}

\algnewcommand\algorithmicupon{\textbf{upon}}
% \algnewcommand\algorithmicdo{\textbf{do}}
\algdef{SE}[UPON]{Upon}{EndUpon}[1]{%
  \algorithmicupon\ #1\ \algorithmicdo%
}{\textbf{end upon}}

\usepackage{tikz}
\graphicspath{{diagrams/out}}
\usepackage{xspace}
% \usepackage{plantuml}

\usepackage[fr-FR]{datetime2}

\usepackage{fancyhdr}
\pagestyle{fancy}
\fancyhf{}
\fancyfoot[L]{Compilé le \DTMnow}
\fancyfoot[C]{\thepage}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}{Definition}
\theoremstyle{remark}
\newtheorem{remark}{Remark}

\newcommand{\RB}{\textsf{RB}\xspace}
\newcommand{\res}{\mathsf{res}}
\newcommand{\ARB}{\textsf{ARB}\xspace}
\newcommand{\DL}{\textsf{DL}}
\newcommand{\APPEND}{\textsf{APPEND}}
\newcommand{\PROVE}{\textsf{PROVE}}
\newcommand{\PROVEtrace}{\textsf{prove}}
\newcommand{\READ}{\textsf{READ}}

\newcommand{\BFTAPPEND}{\textsf{BFT\text{-}APPEND}}
\newcommand{\BFTPROVE}{\textsf{BFT\text{-}PROVE}}
\newcommand{\BFTREAD}{\textsf{BFT\text{-}READ}}


\newcommand{\ABbroadcast}{\textsf{AB-broadcast}}
\newcommand{\ABdeliver}{\textsf{AB-deliver}}
\newcommand{\RBcast}{\textsf{RB-cast}}
\newcommand{\RBreceived}{\textsf{RB-received}}
\newcommand{\ordered}{\textsf{ordered}}
\newcommand{\Winners}{\mathsf{Winners}}
\newcommand{\Messages}{\mathsf{Messages}}
\newcommand{\ABlisten}{\textsf{AB-listen}}

\newcommand{\CANDIDATE}{\textsf{VOTE}}
\newcommand{\CLOSE}{\textsf{COMMIT}}
\newcommand{\READGE}{\textsf{RESULT}}

\newcommand{\SHARE}{\mathsf{SHARE}}
\newcommand{\COMBINE}{\mathsf{COMBINE}}
\newcommand{\VERIFY}{\mathsf{VERIFY}}

\newcommand{\RETRIEVE}{\mathsf{RETRIEVE}}
\newcommand{\SUBMIT}{\mathsf{SUBMIT}}

\newcommand{\delivered}{\mathsf{delivered}}
\newcommand{\received}{\mathsf{received}}
\newcommand{\prop}{\mathsf{prop}}
\newcommand{\resolved}{\mathsf{resolved}}
\newcommand{\current}{\mathsf{current}}

\newcommand{\Seq}{\mathsf{Seq}}
\newcommand{\GE}{\mathsf{GE}}
\newcommand{\BFTDL}{\textsf{BFT\text{-}DL}}

\newcommand{\BFTGE}{\textsf{BFT\text{-}GE}}
\newcommand{\BFTVOTE}{\textsf{BFT\text{-}VOTE}}
\newcommand{\BFTCOMMIT}{\textsf{BFT\text{-}COMMIT}}
\newcommand{\BFTRESULT}{\textsf{BFT\text{-}RESULT}}


\crefname{theorem}{Theorem}{Theorems}
\crefname{lemma}{Lemma}{Lemmas}
\crefname{definition}{Definition}{Definitions}
\crefname{algorithm}{Algorithm}{Algorithms}
% Code exécuté par tout processus p_i

\begin{document}

\section{Model}
We consider a static set of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable. 

\paragraph{Synchrony.} The network is asynchronous. Processes may crash; at most $f$ crashes occur.

\paragraph{Communication.} Processes can exchange through a Reliable Broadcast (\RB) primitive (defined below) which's invoked with the functions \RBcast$(m)$ and \RBreceived$(m)$. There exists a shared object called DenyList (\DL) (defined below) that is interfaced with the functions \APPEND$(x)$, \PROVE$(x)$ and \READ$()$. 

\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $\Pi_M \subseteq \Pi$ (processes allowed to issue \APPEND) and $\Pi_V \subseteq \Pi$ (processes allowed to issue \PROVE). Indices $i,j \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec$ for the \DL{} linearization: $x \prec y$ means that operation $x$ appears strictly before $y$ in the linearized history of \DL. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes). For any round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.

\section{Primitives}

\input{2_Primitives/index.tex}

\section{Target Abstraction: Atomic Reliable Broadcast (ARB)}

\input{3_ARB_Def/index.tex}

\section{ARB over RB and DL}

\input{4_ARB_with_RB_DL/index.tex}

\section{BFT-ARB over RB and DL}

\input{5_BFT_ARB/index.tex}




\section{Implementation of BFT-DenyList and Threshold Cryptography}

\subsection{DenyList}

\paragraph{BFT-DenyList}
In our algorithm we use multiple DenyList as follows:

\begin{itemize}
  \item Let $\mathcal{DL} = \{DL_1, \dots, DL_k\}$ be the set of DenyList used by the algorithm.
  \item We set $k = \binom{n}{f}$.
  \item For each $i \in \{1,\dots,k\}$, let $M_i$ be the set of moderators associated with $DL_i$ according to the DenyList definition, so that $|M_i| = n-f$.
  \item Let $\mathcal{M} = \{M_1, \dots, M_k\}$. We require that the $M_i$ are pairwise distinct:
        \[
          \forall i,j \in \{1,\dots,k\},\ i \neq j \implies M_i \neq M_j.
        \]
\end{itemize}


\begin{lemma}
  $\exists M_i \in M :  \forall p \in M_i$ $p$ is correct.
\end{lemma}

\begin{proof}
  Let consider the set $F$ of faulty processes, with $|F| = f$. We can construct the set $M_i = \Pi \setminus F$ such that $|M_i| = n - |F| = n - f$. By construction, $\forall p \in M_i$ $p$ is correct.
\end{proof}

\begin{lemma}
  $\forall M_i \in M, \exists p \in M_i$ such that $p$ is correct.  
\end{lemma}

\begin{proof}
  $\forall i \in \{1, \dots, k\}, |M_i| = n-f$ with $n \geq 2f+1$. We can say that $|M_i| \geq 2f+1-f = f+1 > f$
\end{proof}

Each process can invoke the following functions :

\begin{itemize}
  \item $\READ' : () \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$
  \item $\APPEND' : \mathbb{R} \rightarrow ()$
  \item $\PROVE' : \mathbb{R} \rightarrow \{0, 1\}$
\end{itemize}

Such that :

\begin{algorithm}[H]
  \caption{$\READ'() \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$}
  \begin{algorithmic}
    \Function{READ'}{}
    \State $j \gets$ the process invoking $\READ'()$
    \State $res \gets \emptyset$
    \ForAll{$i \in \{1, \dots, k\}$}
      \State $res \gets res \cup DL_i.\READ()$
    \EndFor
    \State \Return $res$
    \EndFunction
  \end{algorithmic}
\end{algorithm}

\begin{algorithm}[H]
  \caption{$\APPEND'(\sigma) \rightarrow ()$}
  \begin{algorithmic}
    \Function{APPEND'}{$\sigma$}
    \State $j \gets$ the process invoking $\APPEND'(\sigma)$
    \ForAll{$M_i \in \{M_k \in  M : j \in M_k\}$}
      \State $DL_i.\APPEND(\sigma)$
    \EndFor
    \EndFunction
  \end{algorithmic}
\end{algorithm}

\begin{algorithm}[H]
  \caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$}
  \begin{algorithmic}
    \Function{PROVE'}{$\sigma$}
    \State $j \gets$ the process invoking $\PROVE'(\sigma)$
    \State $flag \gets false$
    \ForAll{$i \in \{1, \dots, k\}$}
      \State $flag \gets flag$ OR $DL_i.\PROVE(\sigma)$
    \EndFor
    \State \Return $flag$
    \EndFunction
  \end{algorithmic}
\end{algorithm}

\subsection{Threshold Cryptography}

We are using the Boneh-Lynn-Shacham scheme as cryptography primitive to our threshold signature scheme.
With :

\begin{itemize}
  \item $G : \mathbb{R} \rightarrow \mathbb{R} \times \mathbb{R} $
  \item $S : \mathbb{R} \times \mathcal{R} \rightarrow \mathbb{R} $
  \item $V : \mathbb{R} \times \mathcal{R} \times \mathbb{R} \rightarrow \{0, 1\} $
\end{itemize}

Such that :

\begin{itemize}
  \item $G(x) \rightarrow (pk, sk)$ : where $x$ is a random value such that $\nexists x_1, x_2: x_1 \neq x_2, G(x_1) = G(x_2)$
  \item $S(sk, m) \rightarrow \sigma_m$
  \item $V(pk, m_1, \sigma_{m_2}) \rightarrow k$ : with $k = 1$ iff $m_1 == m_2$ and $\exists x \in \mathbb{R}$ such that $G(x) \rightarrow (pk, sk)$; otherwise $k = 0$
\end{itemize}

\paragraph{threshold Scheme}

In our algorithm we are only using the following functions :

\begin{itemize}
  \item $G' : \mathbb{R} \times \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{R} \times (\mathbb{R} \times \mathbb{R})^n$ : with $n \triangleq |\Pi|$
  \item $S' : \mathbb{R} \times \mathcal{R} \rightarrow \mathbb{R}$
  \item $C' : \mathbb{R}^n \times \mathcal{R} \times \mathbb{R} \times \mathbb{R}^t \rightarrow \{\mathbb{R}, \bot\}$ : with $t \leq n$
  \item $V' : \mathbb{R} \times \mathcal{R} \times \mathbb{R} \rightarrow \{0, 1\}$
\end{itemize}

Such that :

\begin{itemize}
  \item $G'(x, n, t) \rightarrow (pk, pk_1, sk_1, \dots, pk_n, sk_n)$ : let define $pkc = {pk_1, \dots, pk_n}$
  \item $S'(sk_i, m) \rightarrow \sigma_m^i$
  \item $C'(pkc, m_1, J, \{\sigma_{m_2}^j\}_{j \in J}) \rightarrow \sigma$ : with $J \subseteq \Pi$; and $\sigma = \sigma_{m_1}$ iff $|J| \geq t, \forall j \in J: V(pk_j, m_1, \sigma_{m_2}^j) == 1$; otherwise $\sigma = \bot$.
  \item $V'(pk, m_1, \sigma_{m_2}) \rightarrow V(pk, m_1, \sigma_{m_2})$
\end{itemize}


\bibliographystyle{plain}
\begin{thebibliography}{9}
% (left intentionally blank)
\bibitem{Schneider90}
Fred B.~Schneider.
\newblock Implementing fault-tolerant services using the state machine
  approach: a tutorial.
\newblock {\em ACM Computing Surveys}, 22(4):299--319, 1990.
\end{thebibliography}

\end{document}
