From 5f6278f6e4dc9ad958ce71d44c472408fe67b4f2 Mon Sep 17 00:00:00 2001 From: thibauth Date: Wed, 25 May 2011 06:52:09 +0000 Subject: 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 --- stage/article.tex | 61 +++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file 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 -- cgit v1.2.3-70-g09d2