semi-fresh start on the pacemaker2 specification

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

2 files changed, 257 insertions, 0 deletions

diff --git a/stage/Makefile b/stage/Makefile
new file mode 100644
index 0000000..ffe39be
--- /dev/null
+++ b/stage/Makefile
@@ -0,0 +1,35 @@
+FILE=article
+SOURCES=$(FILE).tex
+BUILD_DIR=build
+
+LATEX=latex
+DVIPS=dvips
+PS2PDF=ps2pdf
+
+all: $(BUILD_DIR)/$(FILE).pdf
+dvi: $(BUILD_DIR)/$(FILE).dvi
+ps: $(BUILD_DIR)/$(FILE).ps
+pdf: $(BUILD_DIR)/$(FILE).pdf
+clean:
+	rm -rf $(BUILD_DIR)
+
+$(BUILD_DIR)/$(FILE).dvi: $(SOURCES)
+
+$(BUILD_DIR):
+	mkdir $@
+
+%.ps: %.dvi
+	$(DVIPS) -o $@ $<
+
+%.pdf: %.ps
+	$(PS2PDF) $< $@
+
+%.dvi: %.tex
+	$(LATEX) $<
+
+$(BUILD_DIR)/%.dvi: %.tex $(BUILD_DIR)
+	$(LATEX) --output-directory=$(BUILD_DIR) $<
+
+
+
+
diff --git a/stage/article.tex b/stage/article.tex
new file mode 100644
index 0000000..56ad427
--- /dev/null
+++ b/stage/article.tex
@@ -0,0 +1,222 @@
+\documentclass[a4paper,10pt]{article}
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage{listings}
+\lstset{escapechar=?, mathescape=true}
+
+\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}%
+}
+
+\begin{document}
+
+\maketitle
+
+\section{Base protocol}
+
+\subsection{Principle}
+
+\begin{itemize}
+  \item{\bf Phase 1:} The server generates a unique seed and initiates
+  a seed pulse which is diffused through the network. Upon receiving the seed,
+  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
+  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. 
+\end{itemize}
+
+\subsection{Messages}
+
+It is assumed that each peer $p$ has a pair of public/private key
+\textsf{(K$^p_{pub}$, K$^p_{priv}$)} and has access to the 3
+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}$}.
+
+ \item{\sf hash(data):} Returns the hash of \textsf{data}.
+\end{itemize}
+
+The key pair of the server will be denoted by \textsf{(KS$_{pub}$,
+KS$_{priv}$)}. \textsf{KS$_{pub}$} is assumed to be known by every peer. 
+
+The following messages are used in the protocol :
+\begin{itemize}
+  \item{\sf Seed($i$, seed$^i$, S$^i_{seed}$):} used to diffuse the seed
+  pulse during phase 1, where:
+  \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}$)}.
+  \end{itemize}
+  
+  \item{\sf SeedReply($i$, H$_p$):} used to build the hash tree during Phase 2,
+  where \textsf{H$_p$} is the token received from peer $p$, that is, the hash of
+  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 round $i$.
+  
+  \item{\sf Proof($i$, seed$^i$, branch$^i$, S$^i_{pulse}$, S$^i_p$):} to answer
+  a challenge.
+\end{itemize}
+
+
+\subsection{Protocol}
+
+\begin{handler}{server-init}{Server at round $i$}{}
+\begin{lstlisting}
+  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 map$^i$ = $\emptyset$
+  $\forall q \in$ NS$_{server}$, send($q$, M$^i_{seed}$);
+
+  wait $T$;
+
+  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}$);
+  $\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}{}
+  if phase$^i$ = Seeding then
+    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}{}
+  if phase$^i$ = Seeding then
+    let H$^i$ = H(map$^i$);
+    let M$^i_{seedreply}$ = SeedReply($i$, H$^i$ );
+    nreplies$^i$ = nreplies$^i$ + 1;
+    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
+    $\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) \}$
+    nreplies$^i$ = 0;
+    phase$^i$ = Seeding;
+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}$ ) 
+  then
+     phase$^i$ = Idle;
+     included$^i$ = $\bot$;
+     if
+       $\exists$ $\{$ $p$ $\rightarrow$ H$^i$ $\}$ $\in$ tree$^i$[level] and
+       $\exists$ $n$ $|$ replies[$n$] = (H$^i$, oldmap$^i$) and
+       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}$)
+       History[$i$] = M$^i_{pulse}$;
+       included$^i$ = $n$;
+       $\forall q \in$ children$^p$, send($q$, Pulse 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}{}
+  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
+    else
+      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}$ )
+\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}$)
+\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}$):
+  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}$ )
+  then
+     good_reply($p$)
+  else
+     bad_reply($p$)
+  end if
+\end{lstlisting}
+\end{handler}
+
+\end{document}
\ No newline at end of file