diff --git a/Recherche/BFT-ARBover/2_Primitives/index.tex b/Recherche/BFT-ARBover/2_Primitives/index.tex index b19dbfb..bd13043 100644 --- a/Recherche/BFT-ARBover/2_Primitives/index.tex +++ b/Recherche/BFT-ARBover/2_Primitives/index.tex @@ -1,12 +1,3 @@ -\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. diff --git a/Recherche/BFT-ARBover/3_ARB_Def/index.tex b/Recherche/BFT-ARBover/3_ARB_Def/index.tex index 7d93751..b5ec715 100644 --- a/Recherche/BFT-ARBover/3_ARB_Def/index.tex +++ b/Recherche/BFT-ARBover/3_ARB_Def/index.tex @@ -1,6 +1,11 @@ -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). \ No newline at end of file +Processes export \ABbroadcast$(m)$ and $m = \ABdeliver()$. \ARB requires the following properties: +\begin{itemize}[leftmargin=*] + \item \textbf{Total Order}: + \begin{equation*} + \forall m_1,m_2,\ \forall p_i,p_j:\ \ (m_1 = \ABdeliver_i()) \prec (m_2 = \ABdeliver_i()) \Rightarrow (m_1 = \ABdeliver_j()) \prec (m_2 = \ABdeliver_j()) + \end{equation*} + \item \textbf{Integrity}: Every message delivered was previously broadcast. $\forall p_i:\ m = \ABdeliver_i() \Rightarrow \exists p_j:\ \ABbroadcast_j(m)$. + \item \textbf{No-duplicates}: No message is delivered more than once at any process. + \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually delivers $m$. +\end{itemize} \ No newline at end of file diff --git a/Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex b/Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex index 98a92c7..6275f04 100644 --- a/Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex +++ b/Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex @@ -1,4 +1,4 @@ -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. +We present below an example of implementation of Atomic Reliable Broadcast (\ARB) using point-to-point reliable, error-free channels and a DenyList (\DL) object according to the model and notations defined in Section 2. \subsection{Algorithm} @@ -28,14 +28,17 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \For{$r = 1, 2, \ldots$}{ \textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\; $S \leftarrow (\unordered \setminus \ordered)$\;\nllabel{code:Sconstruction} - $\RBcast(\texttt{PROP}, S, \langle r, i \rangle)$; $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition} + \lForEach{$j \in \Pi$}{ + $\send(\texttt{PROP}, S, \langle r, i \rangle) \textbf{ to } p_j$ + } + $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition} $\winners[r] \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute} \textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$\;\nllabel{code:check-winners-ack} $M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute-dl} - $\ordered \leftarrow \ordered \cdot \ordered(M)$\;\nllabel{code:next-msg-extraction} + $\ordered \leftarrow \ordered \cdot \order(M)$\;\nllabel{code:next-msg-extraction} } \vspace{0.3em} @@ -46,7 +49,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \vspace{0.3em} - \Upon{$\rdeliver(\texttt{PROP}, S, \langle r, j \rangle)$ from process $p_j$}{ + \Upon{$\receive(\texttt{PROP}, S, \langle r, j \rangle)$ from process $p_j$}{ $\unordered \leftarrow \unordered \cup \{S\}$\;\nllabel{code:receivedConstruction} $\prop[r][j] \leftarrow S$\;\nllabel{code:prop-set} } @@ -54,7 +57,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \vspace{0.3em} \Upon{$\ABdeliver()$}{ - \If{$\ordered \setminus \delivered = \emptyset$}{ + \lIf{$\ordered \setminus \delivered = \emptyset$}{ \Return{$\bot$} } let $m$ be the first element in $(\ordered \setminus \delivered$)\;\nllabel{code:adeliver-extract} @@ -109,7 +112,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \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. + For any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r)$ in their \DL view. \end{lemma} \begin{proof} @@ -117,7 +120,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB 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. + Therefore, for any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r )$ in their \DL view. \end{proof} \begin{lemma}[Well-defined winners]\label{lem:winners} @@ -131,7 +134,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \begin{proof} Lets consider a correct process $p_i$ that reach line~\ref{code:Wcompute} to compute $\winners[r]$. \\ By program order, $p_i$ must have executed $\APPEND_i(r)$ at line~\ref{code:submit-proposition} before, which implies by \Cref{def:closed-round} that round $r$ is closed at that point. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\ - By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\_,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:Wcompute} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\_,r)$ such that + By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:Wcompute} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\ \cdot ,r)$ such that \[ \winners[r] = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r \] @@ -150,13 +153,13 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \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(PROP, S^{(i)}, \langle r, i \rangle)$ and hence any correct will eventually set $\prop[r][i]$ to a non-$\bot$ value. + For any closed round $r$, $\forall i \in \Winners_r$, process $p_i$ must have sent messages to all processes $j \in \Pi$, and hence any correct process $p_j$ will eventually receive $p_i$'s message for round $r$ and set $\prop[r][i]$ to a non-$\bot$ value. \end{lemma} \begin{proof}[Proof] - Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there 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(PROP, S^{(i)}, \langle r, i \rangle)$ 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}. + Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exists a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order in Algorithm~\ref{alg:arb-crash}, $p_i$ must have sent messages to all $j \in \Pi$ at line~\ref{code:submit-proposition} before invoking $\PROVE(r)$. + + If $p_i$ is a correct process that completed sending to all processes, then by the reliable and error-free nature of the communication channels, every correct process $p_j$ will eventually receive $p_i$'s message, which sets $\prop[r][i] \leftarrow S$ at line~\ref{code:prop-set}. If $p_i$ crashes before sending to all processes, then $p_i$ cannot invoke a valid $\PROVE_i(r)$ afterwards, contradicting the assumption that $i \in \Winners_r$. Hence $p_i$ must have completed sending to all processes. \end{proof} \begin{definition}[Messages invariant]\label{def:messages-invariant} @@ -174,17 +177,17 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \begin{proof}[Proof] Let take a correct process $p_i$ that computes $M$ at line~\ref{code:Mcompute-dl}. By \Cref{lem:winners}, $p_i$ computation is the winner set $\Winners_r$. - By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line~\ref{code:Mcompute-dl} where $p_i$ computes $M$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, $M = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]$, we have $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$. + By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line~\ref{code:Mcompute-dl} where $p_i$ computes $M$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received messages from every winner $j \in \Winners_r$. By \Cref{lem:winners-propose}, each winner $j$ has sent messages to all processes including $p_i$. Thus, by the reliable and error-free nature of the channels, if $p_i$ is correct, it will eventually receive $j$'s message, setting $\prop^{(i)}[r][j] \neq \bot$ at line~\ref{code:prop-set}. Hence, $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$. \end{proof} \begin{lemma}[Unique proposal per sender per round]\label{lem:unique-proposal} - For any round $r$ and any process $p_i$, $p_i$ invokes at most one $\RBcast(PROP, S, \langle r, i \rangle)$. + For any round $r$ and any process $p_i$, $p_i$ sends messages to all processes at most once for each round. \end{lemma} \begin{proof}[Proof] - In Algorithm~\ref{alg:arb-crash}, the only place where a process $p_i$ can invoke $\RBcast(PROP, S, \langle r, i \rangle)$ is at line~\ref{code:submit-proposition}, which appears inside the main loop indexed by rounds $r = 1, 2, \ldots$. + In Algorithm~\ref{alg:arb-crash}, the only place where a process $p_i$ can send messages to all processes is at line~\ref{code:submit-proposition}, which appears inside the main loop indexed by rounds $r = 1, 2, \ldots$. - Each iteration of this loop processes exactly one round value $r$, and within that iteration, line~\ref{code:submit-proposition} is executed at most once. Since the loop variable $r$ takes each value $1, 2, \ldots$ at most once during the execution, process $p_i$ invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at most once for any given round $r$. + Each iteration of this loop processes exactly one round value $r$, and within that iteration, messages are sent at most once (before the $\PROVE(r)$ and $\APPEND(r)$ calls). Since the loop variable $r$ takes each value $1, 2, \ldots$ at most once during the execution, process $p_i$ sends messages at most once for any given round $r$. \end{proof} \begin{lemma}[Proposal convergence]\label{lem:convergence} @@ -196,31 +199,28 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \begin{proof}[Proof] Let take a correct process $p_i$ that compute $M$ at line~\ref{code:Mcompute-dl}. That implies that $p_i$ has defined $\winners r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $\winners_r = \Winners_r$. \\ - By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(PROP, S^{(j)}, \langle r, j \rangle)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes + By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ sends messages to all processes at most once per round. Thus, $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined as the messages sent by $j$ in that round. Hence, when $p_i$ computes \[ M^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r. \] \end{proof} \begin{lemma}[Inclusion]\label{lem:inclusion} - If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ invokes - \[ - \RBcast(PROP, S, \langle r, j \rangle)\quad\text{for some S with}\quad m\in S. - \] + If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ sends a proposal $S$ to all processes at line~\ref{code:submit-proposition} with $m\in S$. \end{lemma} \begin{proof} Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the handler at line~\ref{code:abbroadcast-add}, $m$ is added to $\unordered$. Since $p_i$ is correct, it continues executing the main loop. - Consider any iteration of the loop where $p_i$ executes line~\ref{code:Sconstruction} while $m \in (\unordered \setminus \ordered)$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at line~\ref{code:submit-proposition}. + Consider any iteration of the loop where $p_i$ executes line~\ref{code:Sconstruction} while $m \in (\unordered \setminus \ordered)$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and sends $S$ to all processes at line~\ref{code:submit-proposition}. We distinguish two cases: \begin{itemize} - \item \textbf{Case 1: $p_i$ is a winner.} If $p_i \in \Winners_r$ for this round $r$, then by \Cref{def:winner-invariant} and program order, $p_i$ has invoked $\RBcast(PROP, S, \langle r, i \rangle)$ with $m \in S$, and the lemma holds with $j = i$. + \item \textbf{Case 1: $p_i$ is a winner.} If $p_i \in \Winners_r$ for this round $r$, then by \Cref{def:winner-invariant} and program order, $p_i$ has sent proposal $S$ to all processes with $m \in S$, and the lemma holds with $j = i$. - \item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then by the \RB \emph{Validity} property, all correct processes eventually \rdeliver $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\unordered$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round. + \item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then $p_i$ is still a correct process, so it has sent its proposal $S$ (containing $m$) to all processes in $\Pi$. By the reliable and error-free nature of the communication channels, all correct processes will eventually receive $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\unordered$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round. - Since there are infinitely many rounds and finitely many processes, and by \Cref{lem:nonempty} every closed round has at least one winner, there must exist a round $r'$ and a correct process $p_j \in \Winners_{r'}$ such that $m \in (\unordered \setminus \ordered)$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ invokes $\RBcast(PROP, S, \langle r', j \rangle)$ with $m \in S$. + Since there are infinitely many rounds and finitely many processes, and by \Cref{lem:nonempty} every closed round has at least one winner, there must exist a round $r'$ and a correct process $p_j \in \Winners_{r'}$ such that $m \in (\unordered \setminus \ordered)$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ sends messages $S$ with $m \in S$ at line~\ref{code:submit-proposition}. \end{itemize} In both cases, there exists a round and a winner whose proposal includes $m$. @@ -239,12 +239,9 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \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(PROP, S, \langle r, j \rangle)\quad\text{with}\quad m\in S. - \] + Let $p_i$ a correct process that invokes $\ABbroadcast(m)$ and $p_q$ a correct process that infinitely invokes $\ABdeliver()$. By \Cref{lem:inclusion}, there exist a closed round $r$ and a correct process $j\in\Winners_r$ such that $p_j$ sends a proposal $S$ to all processes with $m\in S$. - By \Cref{lem:eventual-closure}, when $p_q$ computes $M$ at line~\ref{code:Mcompute-dl}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(PROP, S, \langle r, j \rangle)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes + By \Cref{lem:eventual-closure}, when $p_q$ computes $M$ at line~\ref{code:Mcompute-dl}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ sends messages at most once per round, so $\prop[r][j]$ is uniquely defined as the proposal sent by $j$. Hence, when $p_q$ computes \[ M = \bigcup_{k\in\Winners_r} \prop[r][k], \] @@ -266,13 +263,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \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(PROP, S_1, \langle r_1, k_1 \rangle)\quad\text{with}\quad m_1\in S_1, - \] - \[ - \RBcast(PROP, S_2, \langle r_2, k_2 \rangle)\quad\text{with}\quad m_2\in S_2. - \] + Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists closed rounds $r_1$ and $r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that $p_{k_1}$ and $p_{k_2}$ send proposals $S_1$ and $S_2$ respectively, with $m_1\in S_1$ and $m_2\in S_2$. Let consider two cases : \begin{itemize} @@ -285,32 +276,32 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB \end{proof} \begin{theorem}[\ARB] -Under the assumed $\DL$ synchrony and $\RB$ reliability, the algorithm implements Atomic Reliable Broadcast. +In a crash asynchronous message-passing system with reliable, error-free communication channels, assuming a synchronous DenyList ($\DL$) object, the algorithm implements Atomic Reliable Broadcast. \end{theorem} \begin{proof} - We show that the algorithm satisfies the properties of Atomic Reliable Broadcast under the assumed $\DL$ synchrony and $\RB$ reliability. + We show that the algorithm satisfies the properties of Atomic Reliable Broadcast under the assumed $\DL$ synchrony and reliable channel assumption. First, by \Cref{lem:bcast-termination}, if a correct process invokes $\ABbroadcast(m)$, then it eventually returns from this invocation. Moreover, \Cref{lem:validity} states that if a correct process invokes $\ABbroadcast(m)$, then every correct process that invokes $\ABdeliver()$ infinitely often eventually delivers $m$. This gives the usual Validity property of $\ARB$. - Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from 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. + Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from processes that constructed and sent them in the algorithm. + Every delivered message was previously sent by some process at line~\ref{code:submit-proposition}, so no spurious messages are delivered. In addition, \Cref{lem:no-duplication} states that no correct process delivers the same message more than once. Together, these arguments yield the Integrity and No-duplicates properties required by $\ARB$. For the ordering guarantees, \Cref{lem:total-order} shows that for any two messages $m_1$ and $m_2$ delivered by correct processes, every correct process that delivers both $m_1$ and $m_2$ delivers them in the same order. Hence all correct processes share a common total order on delivered messages. - All the above lemmas are proved under the assumptions that $\DL$ satisfies the required synchrony properties and that the underlying primitive is a Reliable Broadcast ($\RB$) with Integrity, No-duplicates and Validity. + All the above lemmas are proved under the assumptions that $\DL$ satisfies the required synchrony properties and that the communication channels are reliable and error-free (no message loss or corruption). Therefore, under these assumptions, the algorithm satisfies Validity, Integrity/No-duplicates, and total order, and hence implements Atomic Reliable Broadcast, as claimed. \end{proof} \subsection{Reciprocity} % ------------------------------------------------------------------------------ -So far, we assumed the existence of a synchronous DenyList ($\DL$) object and showed how to 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. +So far, we assumed the existence of a synchronous DenyList ($\DL$) object and showed how to build an Atomic Reliable Broadcast ($\ARB$) primitive using reliable, error-free point-to-point channels. We now briefly argue that, conversely, an $\ARB$ primitive is strong enough to implement a synchronous $\DL$ object. \xspace @@ -346,7 +337,7 @@ Which are cover by our FIFO-\ARB specification. \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. + \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 diff --git a/Recherche/BFT-ARBover/5_BFT_ARB/index.tex b/Recherche/BFT-ARBover/5_BFT_ARB/index.tex index 2452621..5569516 100644 --- a/Recherche/BFT-ARBover/5_BFT_ARB/index.tex +++ b/Recherche/BFT-ARBover/5_BFT_ARB/index.tex @@ -29,7 +29,7 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD()$ such that : \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 Liveness.} Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, x) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$. \paragraph{READ Anti-Flickering.} Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$. @@ -124,7 +124,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au \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}$. + Let $R$ the result of a $READ()$ operation submit by any correct process. $(i, x) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, x) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, x) \in R^{U^\star}$ implie that there exist a valid $DL_{U^\star}.\PROVE_i(x)$. The for loop in the $\BFTPROVE(x)$ implementation return true iff there at least one valid $DL_{U}.\PROVE_i(x)$ for any $U \in \mathcal{U}$. Hence because there exist a $U^\star$ such that $DL_{U^\star}.\PROVE_i(x)$, there exist a valid $\BFTPROVE_i(x)$. @@ -189,18 +189,18 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au \For{$r = 1, 2, \ldots$}{\nllabel{alg:main-loop} \textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\; $S \gets \unordered \setminus \ordered$; - $\RBcast(i, \texttt{PROP}, S, r)$\; + $\RBcast(\texttt{PROP}, S, \langle i, r \rangle)$\; \textbf{wait until} $|\validated(r)| \geq n - t$\;\nllabel{alg:check-validated} \BlankLine \lForEach{$j \in \Pi$}{ - $\BFTAPPEND(\langle j, r\rangle)$\;\nllabel{alg:append} + $\BFTAPPEND(\langle j, r\rangle)$\nllabel{alg:append} } \lForEach{$j \in \Pi$}{ - $\send(j, \texttt{DONE}, r)$\; + $\send(\texttt{DONE}, r)$ \textbf{ to } $p_j$ } \BlankLine @@ -211,7 +211,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au \BlankLine $M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute} - $\ordered \gets \ordered \cdot \ordered(M)$\; + $\ordered \gets \ordered \cdot \order(M)$\; } \vspace{0.3em} diff --git a/Recherche/BFT-ARBover/main.pdf b/Recherche/BFT-ARBover/main.pdf index 0dbee91..938b244 100644 Binary files a/Recherche/BFT-ARBover/main.pdf and b/Recherche/BFT-ARBover/main.pdf differ diff --git a/Recherche/BFT-ARBover/main.tex b/Recherche/BFT-ARBover/main.tex index c224ccb..de11d77 100644 --- a/Recherche/BFT-ARBover/main.tex +++ b/Recherche/BFT-ARBover/main.tex @@ -48,7 +48,7 @@ \newcommand{\DL}{\textsf{DL}} \newcommand{\append}{\ensuremath{\mathsf{append}}} \newcommand{\prove}{\ensuremath{\mathsf{prove}}} -\newcommand{\PROVEtrace}{\ensuremath{\mathsf{prove}}} +% \newcommand{\PROVEtrace}{\ensuremath{\mathsf{prove}}} \newcommand{\readop}{\ensuremath{\mathsf{read}}} % Backward compatibility aliases @@ -65,7 +65,7 @@ \newcommand{\validated}{\ensuremath{\textsc{validated}}} \newcommand{\rbcast}{\ensuremath{\mathsf{rbcast}}} \newcommand{\rbreceived}{\ensuremath{\mathsf{rreceived}}} -% \newcommand{\ordered}{\ensuremath{\mathsf{order}}} +\newcommand{\order}{\ensuremath{\mathsf{order}}} % Backward compatibility aliases \newcommand{\RBcast}{\rbcast} @@ -117,7 +117,7 @@ We consider a static set $\Pi$ of $n$ processes with known identities, communica \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{Communication.} Processes communicate through reliable, error-free point-to-point channels. Messages sent by a correct process to another correct process are eventually delivered without loss or corruption. 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{Notation.} For any indice $x$ we defined by $\Pi_x$ a subset of $\Pi$. We consider two subsets $\Pi_M$ and $\Pi_V$ two authorization subsets. Indices $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$ 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 operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked by process $p_i$. @@ -132,7 +132,7 @@ For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked \input{3_ARB_Def/index.tex} -\section{ARB over RB and DL} +\section{ARB using DL} \input{4_ARB_with_RB_DL/index.tex} @@ -143,156 +143,156 @@ For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked -\section{Implementation of BFT-DenyList and Threshold Cryptography} +% \section{Implementation of BFT-DenyList and Threshold Cryptography} -\subsection{DenyList} +% \subsection{DenyList} -\paragraph{BFT-DenyList} -In our algorithm we use multiple DenyList as follows: +% \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{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{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{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{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} +% \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 : +% 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} +% \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 : +% 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} % \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} +% $j \gets$ the process invoking $\READ'()$\; +% $\res \gets \emptyset$\; +% \ForAll{$i \in \{1, \dots, k\}$}{ +% $\res \gets \res \cup DL_i.\READ()$\; +% } +% \Return{$\res$}\; +% \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{$\APPEND'(\sigma) \rightarrow ()$} +% $j \gets$ the process invoking $\APPEND'(\sigma)$\; +% \ForAll{$M_i \in \{M_k \in M : j \in M_k\}$}{ +% $DL_i.\APPEND(\sigma)$\; +% } +% \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} +% \begin{algorithm}[H] +% \caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$} +% $j \gets$ the process invoking $\PROVE'(\sigma)$\; +% $\flag \gets false$\; +% \ForAll{$i \in \{1, \dots, k\}$}{ +% $\flag \gets \flag$ OR $DL_i.\PROVE(\sigma)$\; +% } +% \Return{$\flag$}\; +% \end{algorithm} -\begin{algorithm}[H] - \caption{$\READ'() \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$} - $j \gets$ the process invoking $\READ'()$\; - $\res \gets \emptyset$\; - \ForAll{$i \in \{1, \dots, k\}$}{ - $\res \gets \res \cup DL_i.\READ()$\; - } - \Return{$\res$}\; - \end{algorithm} +% \subsection{Threshold Cryptography} - \begin{algorithm}[H] - \caption{$\APPEND'(\sigma) \rightarrow ()$} - $j \gets$ the process invoking $\APPEND'(\sigma)$\; - \ForAll{$M_i \in \{M_k \in M : j \in M_k\}$}{ - $DL_i.\APPEND(\sigma)$\; - } - \end{algorithm} +% We are using the Boneh-Lynn-Shacham scheme as cryptography primitive to our threshold signature scheme. +% With : - \begin{algorithm}[H] - \caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$} - $j \gets$ the process invoking $\PROVE'(\sigma)$\; - $\flag \gets false$\; - \ForAll{$i \in \{1, \dots, k\}$}{ - $\flag \gets \flag$ OR $DL_i.\PROVE(\sigma)$\; - } - \Return{$\flag$}\; - \end{algorithm} +% \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} -\subsection{Threshold Cryptography} +% Such that : -We are using the Boneh-Lynn-Shacham scheme as cryptography primitive to our threshold signature scheme. -With : +% \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} -\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} +% \paragraph{threshold Scheme} -Such that : +% In our algorithm we are only using the following functions : -\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} +% \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} -\paragraph{threshold Scheme} +% Such that : -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} +% \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}