preliminaries.tex

\section{Preliminaries \& Model}\label{sec:prelims}

\noindent
\textbf{Notation.}
We use $[~]$ to denote the empty sequence.
We denote by $|C|$ the length of sequence $C$,
by $C[i]$ the $i^{\textsf{th}}$ (zero-based) element of
sequence $C$, and by $C[-i]$ the $i^{\textsf{th}}$ element
from the end. We use $C[i{:}j]$ to mean the subsequence
of $C$ from the $i^{\textsf{th}}$ element (zero-based inclusive)
to the $j^{\textsf{th}}$ element (zero-based exclusive).
Omitting $i$ takes the sequence to the beginning,
and omitting $j$ takes the sequence to the end.
By $C_1 || C_2$, we mean the concatenation
of sequences $C_1$ and $C_2$.
We use the set notation $B \in C$ to iterate
through a sequence $C$.
We use the set builder notation $[B \in C: p(B)]$
to filter the elements of sequence $C$ that satisfy $p$.
We write $C_1 \preccurlyeq C_2$ when $C_1$ is a prefix
of $C_2$ and $C_1 \prec C_2$ to mean that the prefix is strict.
We write $C_1 \sim C_2$ when
$C_1 \preccurlyeq C_2 \lor C_2 \preccurlyeq C_1$.
We use $\kappa$ to denote the security parameter.

\noindent
\textbf{Model.}
Execution occurs in discrete rounds $1, 2, \ldots$, of polynomial number in the
security parameter $\kappa$.
The protocol is executed by
parties of two types: $n$ \emph{nodes} and an unlimited number of \emph{clients}.
The adversary controls $t$ of the nodes.
Nodes are always online. A client is awakened in some round by the environment,
requires a number of rounds to synchronize with the rest of the peers and may be killed by
the environment at a later round.
In each round, the environment invokes \execute
on all honest parties and also triggers the adversary.
We assume all parties have a \emph{global clock}, meaning
they can use the environment function \now to get the current
execution round. We work in two network settings: synchrony and partial synchrony.

\begin{definition}[Synchrony]
  A network is \emph{synchronous} when
  all honestly produced messages are delivered with a delay of at most $\Delta$ rounds
  (messages sent during round $r$ arrive by the beginning of round $r + \Delta$).
\end{definition}

\begin{definition}[Partial Synchrony]
  A network is \emph{partially synchronous} when the adversary can delay
  messages arbitrarily before a Global Stabilization Time (GST)~\cite{dwork1988consensus}; however
  after GST the network becomes synchronous.
\end{definition}

We now turn our attention to distributed ledger protocols, of which blockchain protocols are examples.

\begin{definition}[Ledger]
  A \emph{ledger} is a finite sequence of transactions.
\end{definition}

\begin{definition}[Distributed Ledger Protocol]
  A \emph{distributed ledger protocol} is an
  interactive Turing machine\footnote{%
The ITM captures the behavior (code) of an honest party in the protocol, and
an \emph{execution} contains multiple honest Interactive Turing Machine Instances (ITIs)
all running the same code~\cite{uc}.}
  which exposes the following
  methods on each party:
  \begin{itemize}
    \item $\execute()$: executes a single round of the protocol, during
      which the machine can communicate with the network.
    \item $\wwrite(\tx)$: takes transaction $\tx$ as input.
    \item $\rread()$: outputs a ledger.
  \end{itemize}
\end{definition}

The notation
$\Ledger[][P][r]$ denotes the output of $\rread$
invoked on party $P$ at the end of round $r$.

\begin{definition}[Stickiness]
  A distributed ledger protocol execution is \emph{sticky} if
  for any honest party $P$ and any rounds $r_1 \leq r_2$,
  it holds that $\Ledger[][P][r_1] \preccurlyeq \Ledger[][P][r_2]$.
\end{definition}

%TODO: Stickiness is probably unused in the proofs. Remove if this is indeed the case.
%      Chain safety is required in the proofs.
\begin{definition}[Safety]
  A distributed ledger protocol execution is \emph{safe} if it is sticky and
  for any honest parties $P_1, P_2$ and any rounds $r_1, r_2$, it holds that
  $\Ledger[][P_1][r_1]~\sim~\Ledger[][P_2][r_2]$.
\end{definition}

Stickiness can be easily enforced in any safe protocol
without stickiness by having the parties report the longest
ledger they have seen so far~\cite{streamlet}.

\begin{definition}[Liveness in Synchrony]
  A distributed ledger protocol execution, in a synchronous network, is \emph{live}$(u)$ if
  all transactions written to any honest party
  at round $r$, appear in the ledgers of all honest parties by round
  $r + u$.
\end{definition}

\begin{definition}[Liveness in Partial Synchrony]
  A distributed ledger protocol execution, in a partially synchronous network,
  is \emph{live}$(u)$ if all transactions written to any honest party
  at round $r$, appear in the ledgers of all honest parties by round
  $\max{(r,\gst)} + u$.
\end{definition}