path: root/stage/article.tex

\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, captionpos=b, numbers=left, framexleftmargin=2em, stepnumber=2}
\renewcommand{\lstlistingname}{Spec.}

\usepackage{amsthm}
\newtheorem{thm}{Theorem}


\title{Pacemaker}

\begin{document}

\maketitle

\section{Protocol}

\subsection{Assumptions and notations}

It is assumed that each peer $p$ has a pair of public/private key
\textsf{(K$^p_{pub}$, K$^p_{priv}$)} and has access to the 3
following cryptographic primitives:
\begin{itemize}
 \item{\sf sign(data, K$_{priv}$):} Returns a signature for \textsf{data} 
 using the private key \textsf{K$_{priv}$}.
 \item{\sf verify(S, data, K$_{pub}$):} Verifies that \textsf{S} is a
 signature for \textsf{data} that was created using the private key
 \textsf{K$_{priv}$} associated with \textsf{K$_{pub}$}.
 \item{\sf hash(data):} Returns the hash of \textsf{data}.
\end{itemize}

The key pair of the server will be denoted by \textsf{(KS$_{pub}$,
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.

\subsection{Principle}

The protcol works in three phases:

\subsubsection*{Phase 1: Seeding}

The server generates a unique seed and initiates
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^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^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}

Each peer starts collecting the tokens of his
neighbors and adds his own token to the collected hashes, obtaining a
peer-token map. The hash of this map yields a new token which is sent back to
the neighbors. This progressively builds a hash graph, until the root
server itself hashes the tokens of its children. 

\textsf{SeedReply($i$, H$_p$)} is used to build the hash graph during this phase,
where \textsf{H$_p$} is the token sent by peer $p$, that is, the hash of
the collected map of the tokens received by peer $p$.

\subsubsection*{Phase 3: Pulse}

The server initiates a new pulse with the map it has
collected from its childrens. Upon receiving the pulse, each peer adds to the
pulse the map associated with the token that has been collected during 
Phase 2. Thus, each peer receives a list of hash maps
corresponding to a path from the root to himself in the hash graph computed during Phase 2.

\textsf{Pulse($i$, seed$^i$, branch$^i$, S$^i_{pulse}$)} is used to diffuse the pulse during this
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}$)}.
\end{itemize}

\subsubsection*{Challenges}

The protocol also provides the following request/reply logic to challenge the
availability of a peer:

\begin{itemize}
  \item{\sf Availability($i$, bits):} used by a peer to send his avaibility
  history up to round $i$. \textsf{bits} is a bit array where a $0$ (resp. 1)
  bit at index $j$ means that the peer was absent (resp. available) during round
  $j$.
  \item{\sf Challenge($i$):} used to ask a peer the proof of his presence
  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}$)}.
\end{itemize}

\subsection{Phase 1: Seeding}

\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}$);
  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^i$;
\end{lstlisting}

\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}$)
  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 map$^i$ = {$p \rightarrow$hash(S$^i_p$)};
    let nreplies$^i$ = 0;
    let replies$^i$ = $\emptyset$;
    let included$^i$ = $\bot$;
    let duration$^i$ = $T^i$;
    let phase$^i$ = SEEDING;
  end if
\end{lstlisting}

\subsection{Phase 2: Hashing}

\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$);
    nreplies$^i$ = nreplies$^i+1$;
    replies$^i$[nreplies$^i$] = (H$^i$, map$^i$);
    $\forall q \in$ NS$_p$, send($q$, M$^i_{seedreply}$);    
  end if
\end{lstlisting}

\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$;
  end if
\end{lstlisting}

\subsection{Phase 3: Pulse}

\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$;
  branch$^i$[0] = map$^i$;
  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}[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
     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 < n$ and
       $\forall\; n\in$[1..level], hash(branch$^i$[n]) $\in$ branch$^i$[n-1]
     then
       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$;
       $\forall q \in$ NS$_p$, send($q$, M$^i_{pulse}$);
    end if
  end if
\end{lstlisting}

\subsection{Challenges}
\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
      bits$^i$[$x$] := 0;
    else
      bits$^i$[$x$] := 1;
    end if
  end for  
  let M$^i_{avail}$ = Availability($i$, bits);
  send($q$, M$^i_{avail}$);
\end{lstlisting}

\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}[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}[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
  then
     challenge[$q$] = challenge[$q$]$\oplus${$i\rightarrow$ PROVEN};
  else
     challenge[$q$] = challenge[$q$]$\oplus${$i\rightarrow$ WRONG};
  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}