diff options
| -rw-r--r-- | stage/article.tex | 53 |
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 |