Correct a bunch of mistakes. The seeding phase duration now depends on the round number.

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

1 files changed, 29 insertions, 29 deletions

diff --git a/stage/article.tex b/stage/article.tex
index 8e3df34..65ff05a 100644
--- a/stage/article.tex
+++ b/stage/article.tex
@@ -5,7 +5,7 @@
 \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}
+basicstyle=\small, keywordstyle=\bfseries}
 
 
 \title{Pacemaker}
@@ -36,8 +36,8 @@ KS$_{priv}$)}. \textsf{KS$_{pub}$} is assumed to be known by every peer.
 Each peer $p$ knows the list of peers to whom he is connected, this list is denoted by $NS_p$.
 If $q\in NS_p$ then $p$ can send the message $m$ to $q$ using the function \textsf{send($q$, $m$)}.
 
-$\langle a, b, \ldots\rangle$ will be used to denote the serialisation (depending on the implemetation) of
-two or more pieces of data.
+$\langle a|b|\ldots\rangle$ will be used to denote the serialisation
+(depending on the implemetation) of two or more pieces of data.
 
 \subsection{Principle}
 
@@ -50,13 +50,14 @@ a seed pulse which is diffused through the network. Upon receiving the seed,
 each peer signs it with his private key and hashes it. This hash is called the
 \emph{token} of the peer.
 
-\textsf{Seed($i$, seed$^i$, $T$, S$^i_{seed}$)} is used to diffuse the seed
+\textsf{Seed($i$, seed$^i$, $T^i$, S$^i_{seed}$)} is used to diffuse the seed
 pulse during this phase, where:
 \begin{itemize}
-	\item $i$ is the round number.
-	\item \textsf{seed$^i$} is the seed of round $i$.
-	\item $T$ is the duration of the seeding phase.
-	\item \textsf{S$^i_{pulse}$} is \textsf{sign($\langle$$i$, seed$^i$, $T$$\rangle$, KS$_{priv}$)}.
+    \item $i$ is the round number.
+    \item \textsf{seed$^i$} is the seed of round $i$.
+	\item $T^i$ is the duration of the seeding phase.
+	\item \textsf{S$^i_{pulse}$} is
+	\textsf{sign($\langle$$i$|seed$^i$|$T^i\rangle$, KS$_{priv}$)}.
 \end{itemize}
 
 \subsubsection*{Phase 2: Hashing}
@@ -84,7 +85,7 @@ phase, where:
 \begin{itemize}
     \item \textsf{branch$^i$} is a list of hash maps associated to a path from the server
     to the current peer.
-    \item \textsf{S$^i_{pulse}$} is \textsf{sign($\langle$i, seed$^i$, H$^i$$\rangle$, KS$_{priv}$)}.
+    \item \textsf{S$^i_{pulse}$} is \textsf{sign($\langle$i|seed$^i$|H$^i$$\rangle$, KS$_{priv}$)}.
 \end{itemize}
 
 \subsubsection*{Challenges}
@@ -101,8 +102,7 @@ availability of a peer:
   during round $i$.
   
   \item{\sf Proof($i$, seed$^i$, branch$^i$, S$^i_p$, S$^i_{pulse}$):} to answer
-  a challenge, where \textsf{S$^i_p$} is \textsf{sign($\langle$i, seed$^i$$\rangle$,
-  K$^p_{priv}$)}.
+  a challenge, where \textsf{S$^i_p$} is \textsf{sign($\langle$i|seed$^i$$\rangle$, K$^p_{priv}$)}.
 \end{itemize}
 
 \subsection{Phase 1: Seeding}
@@ -110,34 +110,34 @@ availability of a peer:
 \begin{lstlisting}[title=Server at round $i$]
   let phase$^i$ = SEEDING;
   let seed$^i$ = random_seed();
-  let S$^i_{seed}$ = sign($\langle$$i$,seed$^i$, $T$$\rangle$, KS$_{priv}$);
-  let M$^i_{seed}$ = Seed($i$, seed$^i$, $T$, S$^i_{seed}$);
+  let S$^i_{seed}$ = sign($\langle$$i$|seed$^i$|$T^i$$\rangle$, KS$_{priv}$);
+  let M$^i_{seed}$ = Seed($i$, seed$^i$, $T^i$, S$^i_{seed}$);
   let map$^i$ = $\emptyset$;
   $\forall q \in$ NS$_{server}$, send($q$, M$^i_{seed}$);
 
-  wait $T$;
+  wait $T^i$;
 \end{lstlisting}
 
 \begin{lstlisting}[title={Peer $p$ receiving \textsf{Seed($i$,
-seed$^i$, $T$, S$^i_{seed}$)}}]
+seed$^i$, $T^i$, S$^i_{seed}$)}}]
   if
-    verify(S$^i_{seed}$, $\langle$$i$,seed$^i$,$T$$\rangle$, KS$_{pub}$)
+    verify(S$^i_{seed}$, $\langle$$i$|seed$^i$|$T^i$$\rangle$, KS$_{pub}$)
   then
     $\forall q \in$ NS$_p$, send($q$, M$^i_{seed}$);    
 
-    let S$^i_p$ = sign($\langle$$i$,seed$^i$$\rangle$, K$^p_{priv}$);
+    let S$^i_p$ = sign($\langle$$i$|seed$^i$$\rangle$, K$^p_{priv}$);
     let map$^i$ = {$p \rightarrow$hash(S$^i_p$)};
     let nreplies$^i$ = 0;
     let replies$^i$ = $\emptyset$;
     let included$^i$ = $\bot$;
-    let duration$^i$ = T;
+    let duration$^i$ = $T^i$;
     let phase$^i$ = SEEDING;
   end if
 \end{lstlisting}
 
 \subsection{Phase 2: Hashing}
 
-\begin{lstlisting}[title={Every $\Delta << T$ seconds, on peer $p$}]
+\begin{lstlisting}[title={Every $\Delta << T^i$ seconds, on peer $p$}]
   if phase$^i$ = SEEDING then
     let H$^i$ = hash(map$^i$);
     let M$^i_{seedreply}$ = SeedReply($i$, H$^i$);
@@ -156,29 +156,29 @@ X$_q$)} from peer $q$}]
 
 \subsection{Phase 3: Pulse}
 
-\begin{lstlisting}[title=Server at round $i$ (after having waited $T$)]
+\begin{lstlisting}[title=Server at round $i$ (after having waited $T^i$)]
   phase$^i$ = IDLE;
   let H$^i$ = hash(map$^i$);
   let branch$^i$ = $\emptyset$;
   branch$^i$[0] = map$^i$;
-  let S$^i_{pulse}$ = sign($\langle$$i$,seed$^i$,H$^i$$\rangle$, KS$_{priv}$);
+  let S$^i_{pulse}$ = sign($\langle$$i$|seed$^i$|H$^i$$\rangle$, KS$_{priv}$);
   let M$^i_{pulse}$ = Pulse($i$, seed$^i$, branch$^i$, S$^i_{pulse}$); 
   $\forall q \in$ NS$_{server}$, send($q$, M$^i_{pulse}$);
 \end{lstlisting}
 
 \begin{lstlisting}[title={Peer $p$ receiving \textsf{Pulse($i$, seed$^i$, branch$^i$, S$^i_{pulse}$)}}]
   if
-    verify(S$^i_{pulse}$, $\langle$$i$,seed$^i$,hash(branch$^i$[0])$\rangle$, KS$_{pub}$) 
-  then
+    verify(S$^i_{pulse}$, $\langle$$i$|seed$^i$|hash(branch$^i$[0])$\rangle$,
+    KS$_{pub}$) then
      phase$^i$ = IDLE;
      let level = length(branch$^i$)-1;
      if
        $\exists$ {$p$ $\rightarrow$ H$^i$} $\in$ branch$^i$[level] and
        $\exists\; n\; |$replies[$n$] = (H$^i$, oldmap$^i$) and
-       included$^i$ $$\langle$ n$ and
+       included$^i < n$ and
        $\forall\; n\in$[1..level], hash(branch$^i$[n]) $\in$ branch$^i$[n-1]
      then
-       let branch'$^i$ = branch$^i$[level+1] = oldmap$^i$;
+       branch$^i$[level+1] = oldmap$^i$;
        let M$^i_{pulse}$ = Pulse($i$, seed$^i$, branch'$^i$, S$^i_{pulse}$);
        History[$i$] = ($i$, seed$^i$, branch'$^i$, S$^i_p$, S$^i_{pulse}$);
        included$^i$ = $n$;
@@ -209,16 +209,16 @@ X$_q$)} from peer $q$}]
 
 \begin{lstlisting}[title={Peer $p$ receiving \textsf{Challenge($i$)} from peer
 $q$}]
-  let M$^i_{pulse}$ = Proof(History[$i$]);
-  send($q$, M$^i_{pulse}$);
+  let M$^i_{proof}$ = Proof(History[$i$]);
+  send($q$, M$^i_{proof}$);
 \end{lstlisting}
 
 \begin{lstlisting}[title={Peer $q$ receiving from peer $p$ \textsf{Proof($i$, seed$^i$, branch$^i$, S$^i_p$, S$^i_{pulse}$)}}]
   let level = length(branch$^i$)-1;
   if
      $i$ $\in$ challenges[p] and
-     verify(S$^i_{pulse}$, $\langle$$i$,seed$^i$, hash(branch$^i$[0])$\rangle$, KS$_{pub}$) and
-     verify(S$^i_p$, $\langle$$i$, seed$^i$$\rangle$, K$^p_{pub}$) and
+     verify(S$^i_{pulse}$, $\langle$$i$|seed$^i$|hash(branch$^i$[0])$\rangle$, KS$_{pub}$) and
+     verify(S$^i_p$, $\langle$$i$|seed$^i$$\rangle$, K$^p_{pub}$) and 
      {$p\rightarrow$hash(S$^i_p$)} $\in$ branch$^i$[level] and
      $\forall\; n\in$[1..level], hash(branch$^i$[n]) $\in$ branch$^i$[n-1]
   then