Add the proof of the guarantee given by the protocol.

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

1 files changed, 53 insertions, 8 deletions

diff --git a/stage/article.tex b/stage/article.tex
index b32d3da..c6cc713 100644
--- a/stage/article.tex
+++ b/stage/article.tex
@@ -6,12 +6,14 @@
 \lstdefinelanguage{pseudo}
   {morekeywords={if, then, else, end, let, and, for, in, while}}
 \lstset{escapechar=?, mathescape=true, language=pseudo, frame=single,
-basicstyle=\small, keywordstyle=\bfseries, captionpos=b, numbers=left, framexleftmargin=2em, stepnumber=2}
+basicstyle=\small, keywordstyle=\bfseries, captionpos=b}
 \renewcommand{\lstlistingname}{Spec.}
 
 \usepackage{amsthm}
 \newtheorem{thm}{Theorem}
 
+\theoremstyle{remark}
+\newtheorem*{rem}{Remark}
 
 \title{Pacemaker}
 
@@ -217,15 +219,15 @@ $q$}]
   let M$^i_{proof}$ = Proof(History[$i$]);
   send($q$, M$^i_{proof}$);
 \end{lstlisting}
-
+\newpage
 \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 
-     $\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
+     $\forall\; n\in$[1..level], hash(branch$^i$[n]) $\in$ branch$^i$[n-1] and 
+     {$p\rightarrow$hash(S$^i_p$)} $\in$ branch$^i$[level]
   then
      challenge[$q$] = challenge[$q$]$\oplus${$i\rightarrow$ PROVEN};
   else
@@ -235,7 +237,8 @@ $q$}]
 
 \section{Analysis} 
 
-The first problem to be adressed is the guarentee given by a proof provided by a peer in spec \ref{lst-proof}.
+The first problem to be adressed is the guarantee given by a proof provided by a
+peer in Spec. \ref{lst-proof}.
 
 \begin{thm}
 Assuming that:
@@ -243,16 +246,58 @@ Assuming that:
   \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$.
+Then if peer $p$ provides a valid proof of his presence during round $i$, that
+is a proof satisfying the following four tests:
+\begin{enumerate}
+  \item \emph{verify(S$^i_{pulse}$,
+  $\langle$$i$|seed$^i$|hash(branch$^i$[0])$\rangle$, KS$_{pub}$)}
+  \item \emph{verify(S$^i_p$, $\langle i$|seed$^i\rangle$, K$^p_{pub}$)}
+  \item \emph{$\forall\; n\in$[1..N], hash(branch$^i$[n]) $\in$
+  branch$^i$[n-1]}
+  \item \emph{{$p\rightarrow$hash(S$^i_p$)} $\in$ branch$^i$[N]}
+\end{enumerate}
+then the holder of the proof has the guarantee that $p$ has been communicating
+with at least one other peer during the seeding phase of round $i$ starting at time $t_i$ 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
+\paragraph{First step: S$^i_{p}$ has been computed by $p$ after
+time $t_i$}
+
+Indeed, with test 2 we have the guarantee that S$^i_{p}$ has been computed
+by $p$. Furthermore, at the time of computation $p$ knew the seed
+\textsf{seed$^i$}. This seed has been generated randomly by the server at the
+beginning of round $i$ : this is guaranteed by test 1 and by the integrity of
+the server. Thus the time of computation of S$^i_{p}$ is posterior to $t_i$.
+
+\paragraph{Second step: branch$^i$ has been computed before $t_i+T_i$}
+
+By induction:
+
+\subparagraph{Basis:} Test 1 and the integrity of the server guarantee
+that branch$^i$[0] has been computed before $t_i+T_i$ (the server
+sends branch$^i$[0] at time $t_i+T_i$).
 
+\subparagraph{Inductive Step:} Let us now assume that branch$^i$[0] up to
+branch$^i$[k] have been computed before $t_i+T_i$. We know (test 3)
+that $t=$hash(branch$^i$[k+1])$\in$ branch$^i$[k].
+Now assume by contraction that $m=$branch$^i$[k+1]) has been computed
+after $t_i+T_i$ by some peer $q$. Then given $t$, $q$ has been able to compute
+$m$ such that hash($m$)$=t$ which would be a successful first preimage
+attack on the hash function.
 
+\paragraph{Conclusion:} Using the first two steps and test 4, we now have the
+guarantee that S$^i_{p}$ has been computed by $p$ after $t_i$ and transmitted
+before $t_i+T^i$. Thus $p$ has been communicating with some peer during round
+$i$.
 \end{proof}
 
+\begin{rem}
+Unfortunately we have no guarantee that peer $p$ has been respecting the
+protocol at all. For example he could have just received see$^i$ from a
+colluding peer $q$, computed and sent back S$^i_{p}$ to $q$ who would have
+inserted S$^i_{p}$ in the branch himself.
+\end{rem}
 \end{document}
\ No newline at end of file