Some cleanup in the pacemaker protocol

git-svn-id: https://scm.gforge.inria.fr/svn/pacemaker@7 30fcff6e-8de6-41c7-acce-77ff6d1dd07b

1 files changed, 82 insertions, 93 deletions

diff --git a/stage/article.tex b/stage/article.tex
index 56ad427..e500d96 100644
--- a/stage/article.tex
+++ b/stage/article.tex
@@ -2,31 +2,13 @@
 \usepackage[T1]{fontenc}
 \usepackage[utf8]{inputenc}
 \usepackage{listings}
-\lstset{escapechar=?, mathescape=true}
+\lstdefinelanguage{pseudo}
+  {morekeywords={if, then, else, end, let, and, for, in, while}}
+\lstset{escapechar=?, mathescape=true, language=pseudo, frame=single,
+basicstyle=\sffamily\small, keywordstyle=\sffamily\bfseries}
 
-\title{Pacemaker}
 
-% #1: fig:label
-% #2: Handler title
-% #3: caption
-\newenvironment{handler}[3]{%
-\def\handlerlabel{fig:#1}%
-\def\handlertitle{#2}%
-\def\handlercaption{#3}%
-\begin{figure}[!h]%
-\center\vspace{1em}%
-\noindent\begin{tabular}{|p{\textwidth}|}%
-\hline%
-\footnotesize%
-{\tt\bf \handlertitle}%
-}
-{%
-\\ \hline%
-\end{tabular}%
-\caption{\handlercaption}%
-\label{\handlerlabel}%
-\end{figure}%
-}
+\title{Pacemaker}
 
 \begin{document}
 
@@ -42,15 +24,15 @@
   each peer signs it with its private key and hashes it. This hash is called the
   \emph{token} of the peer.
   \item{\bf Phase 2:} Each peer starts collecting the tokens of its
-  neighbors and joins its own hash, obtaining a \emph{peer-token} map.
-  This map is then hashed and the hash yields a new token which is sent
-  back to the neighbors. This progressively builds a hash tree until the root
+  neighbors and add its own hash to the collected hashes, obtaining a
+  peer-token map. The hash of this map yields a new token which is sent back to
+  the neighbors. This progressively builds a hash tree until the root
   server itselfs hashes the tokens of its children.
   \item{\bf Phase 3:} The server initiates a new pulse with the map it has
   collected from its childrens. Upon receiving the pulse, each peer adds to the
   pulse the map associated with the token that has been collected during 
-  Phase 2. Thus, each peer receives a list of hash maps corresponding to a
-  branch from the root to itself in the hash tree computed during phase 2. 
+  Phase 2. Thus, each peer receives a list of hash maps
+  corresponding to a branch from the root to itself in the hash tree computed during phase 2. 
 \end{itemize}
 
 \subsection{Messages}
@@ -61,7 +43,6 @@ following cryptographic primitives:
 \begin{itemize}
  \item{\sf sign(data, K$_{priv}$):} Returns a signature for \textsf{data} 
  using the private key \textsf{K$_{priv}$}.
- \item 
  \item{\sf verify(S, data, K$_{pub}$):} Verifies that \textsf{S} is a
  signature for \textsf{data} that was created using the private key
  \textsf{K$_{priv}$} associated with \textsf{K$_{pub}$}.
@@ -79,7 +60,7 @@ The following messages are used in the protocol :
   \begin{itemize}
   	\item $i$ is the round number.
   	\item \textsf{seed$^i$} is the seed of round $i$.
-  	\item \textsf{S$^i_{pulse}$} is \textsf{sign(<$i$,seed$^i$>, KS$_{priv}$)}.
+  	\item \textsf{S$^i_{pulse}$} is \textsf{sign(<$i$, seed$^i$>, KS$_{priv}$)}.
   \end{itemize}
   
   \item{\sf SeedReply($i$, H$_p$):} used to build the hash tree during Phase 2,
@@ -87,24 +68,45 @@ The following messages are used in the protocol :
   the collected map of the tokens received by peer $p$.
   
   \item{\sf Pulse($i$, seed$^i$, H$^i$, level, branch$^i$, S$^i_{pulse}$):} used
-  during Phase 3.
-  
-  \item{\sf Challenge($i$, $p$):} used to ask peer $p$ the proof of its presence
+  during Phase 3. Where:
+  \begin{itemize}
+    \item \textsf{H$^i$} is the hash of the map built by the server during
+    phase 2.
+    \item \textsf{level} is the current level in the branch built from the root
+    server to the current peer.
+    \item \textsf{branch$^i$} is a branch of hash maps going from the server
+    to the current peer. This branch is a part of the hash tree built during
+    phase 2.
+    \item \textsf{S$^i_{pulse}$} is \textsf{sign(<i, seed$^i$, H$^i$>, KS$_{priv}$)}
+  \end{itemize}
+\end{itemize}
+ 
+The protocol also provides the following request/reply logic to challenge the
+availability of a peer:
+
+\begin{itemize}
+  \item{\sf Availability($i$, bits):} used by a peer to send its avaibility
+  history up to round $i$. \textsf{bits} is a bit array where a $0$ (resp. 1)
+  bit at index $j$ means that the peer was absent (resp. available) during round
+  $j$.
+  \item{\sf Challenge($i$):} used to ask a peer the proof of its presence
   during round $i$.
   
   \item{\sf Proof($i$, seed$^i$, branch$^i$, S$^i_{pulse}$, S$^i_p$):} to answer
-  a challenge.
+  a challenge, where \textsf{S$^i_p$} is \textsf{sign(<i, seed$^i$>,
+  K$^p_{priv}$)}.
 \end{itemize}
 
+A peer can also choose to send its availability history up to round $i$
 
 \subsection{Protocol}
 
-\begin{handler}{server-init}{Server at round $i$}{}
-\begin{lstlisting}
+\subsubsection{Proof building}
+\begin{lstlisting}[title=Server at round $i$]
   let phase$^i$ = Seeding;
   let seed$^i$ = random_seed();
-  let S$^i_{seed}$ = sign( <$i$,seed$^i$>, KS$_{priv}$);
-  let M$^i_{seed}$ = Seed($i$,seed$^i$,S$^i_{seed}$);
+  let S$^i_{seed}$ = sign(<$i$,seed$^i$>, KS$_{priv}$);
+  let M$^i_{seed}$ = Seed($i$, seed$^i$, S$^i_{seed}$);
   let map$^i$ = $\emptyset$
   $\forall q \in$ NS$_{server}$, send($q$, M$^i_{seed}$);
 
@@ -112,51 +114,47 @@ The following messages are used in the protocol :
 
   phase$^i$ = Idle;
   H$^i$ = Hash(map$^i$);
-  let S$^i_{pulse}$ = sign( <$i$,seed$^i$,H$^i$>, KS$_{priv}$ );
-  let M$^i_{pulse}$ = Pulse($i$, seed$^i$, H$^i$, 
-                     0, $\{$ 0 $\rightarrow$ map$^i$ $\}$, S$^i_{pulse}$);
+  let S$^i_{pulse}$ = sign(<$i$,seed$^i$,H$^i$>, KS$_{priv}$);
+  let M$^i_{pulse}$ = Pulse($i$, seed$^i$, H$^i$, 0, 
+                      $\{$ 0 $\rightarrow$ map$^i$ $\}$, S$^i_{pulse}$); 
   $\forall q \in$ NS$_{server}$, send($q$, M$^i_{pulse}$);
 \end{lstlisting}
-\end{handler}
 
-\begin{handler}{xn}{Server or peer receiving SeedReply ($i$, X$_q$) from peer $q$:}{}
-\begin{lstlisting}{}
+\begin{lstlisting}[title={Server or peer receiving \textsf{SeedReply($i$,
+X$_q$)} from peer $q$}]
   if phase$^i$ = Seeding then
-    map$^i$ = $\{ q \rightarrow $X$_q \} \oplus$ map$^i$;
+    map$^i$ = $\{ q \rightarrow $X$_q \} \oplus$map$^i$;
   end if
 \end{lstlisting}
-\end{handler}
 
-\begin{handler}{xn}{Every $\Delta << T$ seconds, on peer $p$:}{}
-\begin{lstlisting}{}
+\begin{lstlisting}[title={Every $\Delta << T$ seconds, on peer $p$}]
   if phase$^i$ = Seeding then
     let H$^i$ = H(map$^i$);
-    let M$^i_{seedreply}$ = SeedReply($i$, H$^i$ );
+    let M$^i_{seedreply}$ = SeedReply($i$, H$^i$);
     nreplies$^i$ = nreplies$^i$ + 1;
-    replies$^i$[ nreplies$^i$ ] = (H$^i$, map$^i$);
+    replies$^i$[nreplies$^i$] = (H$^i$, map$^i$);
     $\forall q \in$ NS$_p$, send($q$, M$^i_{seedreply}$);    
   end if
 \end{lstlisting}
-\end{handler}
 
-\begin{handler}{x1}{Peer $p$ receiving M$^i_{seed}$ = Seed ($i$,seed$^i$,S$^i_{seed}$):}{}
-\begin{lstlisting}{}
-if verify_sig( S$^i_{seed}$,  <$i$,seed$^i$>, KS$_{priv}$) then
+\begin{lstlisting}[title={Peer $p$ receiving M$^i_{seed}$ = \textsf{Seed($i$,
+seed$^i$, S$^i_{seed}$)}}]
+  if
+    verify_sig(S$^i_{seed}$, <$i$,seed$^i$>, KS$_{pub}$)
+  then
     $\forall q \in$ NS$_p$, send($q$, M$^i_{seed}$);    
 
-    let S$^i_p$ = sign( <$i$,seed$^i$>, K$^p_{priv}$);
-    let map$^i$ = $\{ p \rightarrow H(S^i_p) \}$
+    let S$^i_p$ = sign(<$i$,seed$^i$>, K$^p_{priv}$);
+    let map$^i$ = $\{p \rightarrow H(S^i_p)\}$;
     nreplies$^i$ = 0;
     phase$^i$ = Seeding;
-end if
+  end if
 \end{lstlisting}
-\end{handler}
 
-\begin{handler}{x3}{Peer $p$ receiving
-   Pulse($i$, seed$^i$, H$^i$, level, tree$^i$, S$^i_{pulse}$):}{}
-\begin{lstlisting}{}
-  if 
-     verify_sig(S$^i_{pulse}$, <$i$, seed$^i$, H$^i$ >, KS$_{pub}$ ) 
+\begin{lstlisting}[title={Peer $p$ receiving \textsf{Pulse($i$, seed$^i$, H$^i$,
+level, tree$^i$, S$^i_{pulse}$)}}]
+  if
+    verify_sig(S$^i_{pulse}$, <$i$,seed$^i$,H$^i$>, KS$_{pub}$) 
   then
      phase$^i$ = Idle;
      included$^i$ = $\bot$;
@@ -166,57 +164,48 @@ end if
        included$^i$ $<$ $n$ and
        verify_tree(H$^i$, level, tree$^i$)
      then
-       let tree'$^i$ = tree$^i$ $\oplus$ $\{$ level+1 $\rightarrow$ oldmap$^i$ $\}$;
-       M$^i_{pulse}$ = ($i$, seed$^i$, H$^i$, level+1, tree'$^i$, S$^i_{pulse}$)
+       let tree'$^i$ = tree$^i$$\oplus$$\{$level+1 $\rightarrow$ oldmap$^i$$\}$;
+       let M$^i_{pulse}$ = Pulse($i$, seed$^i$, H$^i$, level+1, tree'$^i$, S$^i_{pulse}$);
        History[$i$] = M$^i_{pulse}$;
        included$^i$ = $n$;
-       $\forall q \in$ children$^p$, send($q$, Pulse M$^i_{pulse}$);
-     end if
+       $\forall q \in$ children$^p$, send($q$, M$^i_{pulse}$);
+    end if
   end if
 \end{lstlisting}
-\end{handler}
 
-\begin{handler}{x4}{Peer $p$ sending to $q$ its availability at round $i$:}{}
-\begin{lstlisting}{}
+\subsubsection{Challenges}
+\begin{lstlisting}[title=Peer $p$ sending to $q$ its availability at round $i$]
   let bits$^i$ = new bitfield[$N_t$];
   for $x$ in [1..$N_t$]
     if History[$i-N_t+x$] = $\emptyset$ then
-      bits$^i$[$x$] := 0
+      bits$^i$[$x$] := 0;
     else
-      bits$^i$[$x$] := 1
+      bits$^i$[$x$] := 1;
     end if
   end for  
-  let S$^i_{avail}$ = sign( < $i$, bits$^i$ >, K$^p_{priv}$ )
-  let M$^i_{avail}$ = ($i$,bits,S$^i_{avail}$);
-  send( $q$, Availability M$^i_{avail}$ )
+  let M$^i_{avail}$ = Availability($i$, bits);
+  send($q$, M$^i_{avail}$)
 \end{lstlisting}
-\end{handler}
 
-\begin{handler}{x5}{Peer $p$ receiving Challenge($i$, nonce) from peer $q$:}{}
-\begin{lstlisting}{}
-  let M$^i_{pulse}$ = History[$i$]
-  send( $q$, Proof M$^i_{pulse}$)
+\begin{lstlisting}[title={Peer $p$ receiving \textsf{Challenge($i$)} from peer
+$q$}]
+  let M$^i_{pulse}$ = History[$i$];
+  send($q$, Proof M$^i_{pulse}$)
 \end{lstlisting}
-\end{handler}
 
-\begin{handler}{x6}{Peer $q$ receiving from peer $p$
-    Proof ($i$, nonce, K$^i_{pub}$, trees$^i$, S$^i_p$, S$^i_{pulse}$, S$_{proof}$):}{}
-\begin{lstlisting}{}
-Peer $q$ receiving from peer $p$
-    Proof ($i$, nonce, K$^i_{pub}$, trees$^i$, S$^i_p$, S$^i_{pulse}$, S$_{proof}$):
+\begin{lstlisting}[title={Peer $q$ receiving from peer $p$ \textsf{Proof($i$, nonce, K$^i_{pub}$, trees$^i$, S$^i_p$, S$^i_{pulse}$, S$_{proof}$)}}]
   if
-     ($i$, nonce, $p$) $\in$ challenges $\land$
-     verify_sig(S$^i_{pulse}$,<$i$, seed$^i$,$K^i_{pub}$,trees$^i$[0]>,KS$_{pub}$) $\land$
-     verify_sig(S$^i_p$, <$i$, seed$^i$ >, K$^p_{pub}$) $\land$
-     S$^i_p$ $\in$ trees$^i$ $\land$
-     $\forall n>0$, H(trees$^i$[n]) $\in$ trees$^i$[n-1] $\land$
-     verify_sig(S$_{proof}$, < nonce, H$^p$, H$^q$ >, K$^i_{pub}$ )
+     ($i$, nonce, $p$) $\in$ challenges and
+     verify_sig(S$^i_{pulse}$, <$i$,seed$^i$,$K^i_{pub}$,trees$^i$[0]>,KS$_{pub}$) and
+     verify_sig(S$^i_p$, <$i$, seed$^i$ >, K$^p_{pub}$) and
+     S$^i_p$ $\in$ trees$^i$ and
+     $\forall n>0$, H(trees$^i$[n]) $\in$ trees$^i$[n-1] and
+     verify_sig(S$_{proof}$, < nonce, H$^p$, H$^q$ >, K$^i_{pub}$)
   then
      good_reply($p$)
   else
      bad_reply($p$)
   end if
 \end{lstlisting}
-\end{handler}
 
 \end{document}
\ No newline at end of file