Add line numbers to listings, add caption numbers to listings to allow references, beginning of the analysis section

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

1 files changed, 40 insertions, 13 deletions

diff --git a/stage/article.tex b/stage/article.tex
index 65ff05a..b32d3da 100644
--- a/stage/article.tex
+++ b/stage/article.tex
@@ -1,11 +1,16 @@
 \documentclass[a4paper,10pt]{article}
 \usepackage[T1]{fontenc}
 \usepackage[utf8]{inputenc}
+
 \usepackage{listings}
 \lstdefinelanguage{pseudo}
   {morekeywords={if, then, else, end, let, and, for, in, while}}
 \lstset{escapechar=?, mathescape=true, language=pseudo, frame=single,
-basicstyle=\small, keywordstyle=\bfseries}
+basicstyle=\small, keywordstyle=\bfseries, captionpos=b, numbers=left, framexleftmargin=2em, stepnumber=2}
+\renewcommand{\lstlistingname}{Spec.}
+
+\usepackage{amsthm}
+\newtheorem{thm}{Theorem}
 
 
 \title{Pacemaker}
@@ -107,7 +112,7 @@ availability of a peer:
 
 \subsection{Phase 1: Seeding}
 
-\begin{lstlisting}[title=Server at round $i$]
+\begin{lstlisting}[caption=Server at round $i$]
   let phase$^i$ = SEEDING;
   let seed$^i$ = random_seed();
   let S$^i_{seed}$ = sign($\langle$$i$|seed$^i$|$T^i$$\rangle$, KS$_{priv}$);
@@ -118,7 +123,7 @@ availability of a peer:
   wait $T^i$;
 \end{lstlisting}
 
-\begin{lstlisting}[title={Peer $p$ receiving \textsf{Seed($i$,
+\begin{lstlisting}[caption={Peer $p$ receiving \textsf{Seed($i$,
 seed$^i$, $T^i$, S$^i_{seed}$)}}]
   if
     verify(S$^i_{seed}$, $\langle$$i$|seed$^i$|$T^i$$\rangle$, KS$_{pub}$)
@@ -137,7 +142,7 @@ seed$^i$, $T^i$, S$^i_{seed}$)}}]
 
 \subsection{Phase 2: Hashing}
 
-\begin{lstlisting}[title={Every $\Delta << T^i$ seconds, on peer $p$}]
+\begin{lstlisting}[caption={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$);
@@ -147,7 +152,7 @@ seed$^i$, $T^i$, S$^i_{seed}$)}}]
   end if
 \end{lstlisting}
 
-\begin{lstlisting}[title={Server or peer receiving \textsf{SeedReply($i$,
+\begin{lstlisting}[caption={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$;
@@ -156,7 +161,7 @@ X$_q$)} from peer $q$}]
 
 \subsection{Phase 3: Pulse}
 
-\begin{lstlisting}[title=Server at round $i$ (after having waited $T^i$)]
+\begin{lstlisting}[caption=Server at round $i$ (after having waited $T^i$)]
   phase$^i$ = IDLE;
   let H$^i$ = hash(map$^i$);
   let branch$^i$ = $\emptyset$;
@@ -166,7 +171,7 @@ X$_q$)} from peer $q$}]
   $\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}$)}}]
+\begin{lstlisting}[caption={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
@@ -188,7 +193,7 @@ X$_q$)} from peer $q$}]
 \end{lstlisting}
 
 \subsection{Challenges}
-\begin{lstlisting}[title=Peer $p$ sending to $q$ his availability at round $i$ over the last $N_t$ rounds]
+\begin{lstlisting}[caption=Peer $p$ sending to $q$ his availability over the last $N_t$ rounds]
   let bits$^i$ = new bitfield[$N_t$];
   for $x$ in [1..$N_t$]
     if History[$i-N_t+x$] = $\emptyset$ then
@@ -201,26 +206,26 @@ X$_q$)} from peer $q$}]
   send($q$, M$^i_{avail}$);
 \end{lstlisting}
 
-\begin{lstlisting}[title={Peer $p$ sending to $q$ \textsf{Challenge($i$)}}]
+\begin{lstlisting}[caption={Peer $p$ sending to $q$ \textsf{Challenge($i$)}}]
   challenges[$q$] = challenges[$q$]$\oplus${$i\rightarrow$ WAITING};
   let M$^i_{challenge}$ = Challenge($i$);
   send($q$, M$^i_{challenge}$);
 \end{lstlisting}
 
-\begin{lstlisting}[title={Peer $p$ receiving \textsf{Challenge($i$)} from peer
+\begin{lstlisting}[caption={Peer $p$ receiving \textsf{Challenge($i$)} from peer
 $q$}]
   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}$)}}]
+\begin{lstlisting}[caption={Peer $q$ receiving from peer $p$ \textsf{Proof($i$, seed$^i$, branch$^i$, S$^i_p$, S$^i_{pulse}$)}}, label=lst-proof]
   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 
-     {$p\rightarrow$hash(S$^i_p$)} $\in$ branch$^i$[level] and
+     verify(S$^i_p$, $\langle i$|seed$^i\rangle$, K$^p_{pub}$) and 
      $\forall\; n\in$[1..level], hash(branch$^i$[n]) $\in$ branch$^i$[n-1]
+     {$p\rightarrow$hash(S$^i_p$)} $\in$ branch$^i$[level] and
   then
      challenge[$q$] = challenge[$q$]$\oplus${$i\rightarrow$ PROVEN};
   else
@@ -228,4 +233,26 @@ $q$}]
   end if
 \end{lstlisting}
 
+\section{Analysis} 
+
+The first problem to be adressed is the guarentee given by a proof provided by a peer in spec \ref{lst-proof}.
+
+\begin{thm}
+Assuming that:
+\begin{itemize}
+  \item the server is not corrupted
+  \item peers do not share private keys
+\end{itemize}
+Then if peer $p$ provides a valid proof of his presence during round $i$ then $p$ has been communicating with
+at least one other peer during the seeding phase of round $i$ starting at time $ti$ and ending at time $t_i+T^i$.
+\end{thm}
+
+\begin{proof}
+Let ($i$, seed$^i$, branch$^i$, S$^i_p$, S$^i_{pulse}$) be the proof provided by peer $p$.
+
+\paragraph{First step:} S$^i_{pulse}$ has been computed after time $t_i$. Indeed, with the first
+
+
+\end{proof}
+
 \end{document}
\ No newline at end of file