protocol.tex

We now sketch an implementation of the specification from
Chapter~\ref{Chapter:Spec}: a simple voting protocol based on linkable ring
signatures \cite{lrs}, on top of a Hardened Dissent \cite{sec} instance that
provides instigator anonymity, along with acccountability to handle byzantine
faults.
\section{Building Blocks}
We combine several existing cryptosystems and distributed systems to construct
our protocol.
\subsection{Hardened Dissent}
A security analysis of the original peer-to-peer Dissent resulted in a modified
protocol providing the following properties:
  \begin{theorem} At the end of turn $\turn$, either all participants see the
    same value of all messages, any peers disrupting the protocol are detected
    and eliminated, or the round does not terminate.\todo{TODO: explain}%\ldots
    \todo{semicomputability}
  \end{theorem}
  \begin{theorem} For any turn $\turn$, all participants know the results of
    round $\turn$ before any know the results of round
    $\turn+1$.\end{theorem}\label{theorem:rounds}
  \begin{theorem}[Anonymity] When Hardened Dissent is executed and completes in
    a cluster of $\NumClients$ participants, of which $\NumHonest$ are honest,
    none of the avenues of attack descibed in our threat models\ldots provide
    non-negligable advantage over uniform guessing in determining which of the
    $\NumHonest$ honest participants sent any particular message.
  \end{theorem}\label{theorem:anon}
  All properties are rigorously proven in \cite{sec}.

This satisfies the specification for an anonymous messaging protocol given in
Section~\ref{Section:AnonBcastP}.
% \todo{TODO: talk about accountability?}
% Further, using this protocol justifies our

\subsection{Linkable Ring Signatures}
Our voting protocol is based on the concept of a linkable ring signature (LRS),
introduced in \cite{lrs}. The documentation of the CryptoBook implementation in
Go explains:
\begin{quote}
 ``The caller supplies one or more public keys representing an anonymity set,
 and the private key corresponding to one of those public keys. The resulting
 signature proves to a verifier that the owner of one of these public keys
 signed the message, without revealing which key-holder signed the message,
 offering anonymity among the members of this explicit anonymity set. The other
 users whose keys are listed in the anonymity set need not consent or even be
 aware that they have been included in an anonymity set: anyone having a
 suitable public key may be "conscripted" into a set.

 [\ldots]

  [G]iven two signatures produced using the same linkScope, a verifier will be
  able to tell whether the same or different anonymity set members produced
  those signatures. In particular, verifying a linkable signature yields a
  linkage tag.  This linkage tag has a 1-to-1 correspondence with the signer's
  public key within a given linkScope, but is cryptographically unlinkable to
  either the signer's public key or to linkage tags in other scopes. \ldots
  Linkage tags may be used to protect against sock-puppetry or Sybil attacks in
  situations where a verifier needs to know how many distinct members of an
  anonymity set are present or signed messages in a given context.
\end{quote}
\cite{golrs}
% \toadd{explain in own words instead of having a page and a half long quote}
\section{Algorithms}
\subsection{Initial formation}
We assume the member set is well known, that every member has a secure channel
through which it can communicate with every other member, and that members
remain connected. Initially, the members organize themselves into a Peer-to-Peer
Dissent cluster \cite{p2pd} using some consensus protocol such as Byzantine
Paxos, as discussed in \cite{sec}.

% The Dissent configuration file specifies the size and ordering of clients'
% message slots\todogrunt{Need to define client and slot somewhere}. which will
% consist of, for each of the $\NumClients$ clients: space for a \StructBallot,
% and space for up to $\NumClients$ signatures so the client can sign whatever
% other proposals are in play.  We only allow any given client to have one
% proposal at any given time.
%
% \subsection{Peer-to-Peer Layer}
Initially, the \KwManifest~of the Petition protocol layer includes all \KwNode s
in the Broadcast layer as \KwMember s of the \KwCluster.

\subsection{Voting with Linkable Ring Signatures}
We now sketch implementations of the functions from
Section~\ref{Subsection:PetitionIface}, using this Hardened Dissent instance as
the underlying anonymous broadcast layer.

To \NamePropose a \StructPetition, a \KwPeer generates a unique \KwLinkScope to
associate with this petition, and specifies a Dissent \KwRound~$\round$~when the
\StructPetition will expire. The instigating peer then broadcasts this petition
to the group.

By associating a unique link scope with each petition, we allow \KwMember s to
vote by producing a signature with the current \KwRoster and the proposer's link
scope. Each \KwMember~that wishes to vote for the petition broadcasts the
petition along with its signature, on any turn before $\round$. Dissent provides
the functionality required for the anonymous broadcast layer, and so given our
reliability assumptions, every \KwMember~will eventually be able to \NameReceive
the \StructElectionState~containing a list of anonymous signatures associated
with the petition. At the specified round $\round$, each member should
\NameEvaluate all signatures received. If the function $\FunEval$ applied to the
set of unique, valid signatures results in \todo{TODO: updtae for ballot
choices}\AtomTrue, then the petition passes.

\toadd{ Illustrate the round message format, which will consist of, for each of
  the $\NumClients$ clients: space for a \texttt{Ballot}, and space for up to
  $\NumClients$ signatures so the client can sign whatever other proposals are
  in play.  We only allow any given client to have one proposal at any given
time.  }
Within a round, each \KwMember~may \todosubst{Jamming by proposing
ballots??? Infinite timeouts???} transmit a \KwPetition. A
\KwPetition~consists of:
\begin{itemize}
  \item A proposed \KwManifest, as described above,
  \item A \KwLinkScope\todogrunt{Explain}
  % \item A collection of \texttt{Signatures}\todogrunt{Explain}
  \item A \KwRound~when the ballot will expire.
\end{itemize}

Once a \KwPetition~has been proposed, the other \KwMember s have the
opportunity to \NameVote. A \KwMember~votes by transmitting the most
recent version of \SetVotes, but with the \texttt{Signatures} field
modified to include the proposed \KwManifest~signed with the voting
\KwMember's private key for this link scope.\toadd{I think this is
wrong}

By the designated expiration round, all \KwMember s have enough
information to determine whether or not the \KwPetition~\emph{passes}:
Each \KwMember~should verify all signatures on the most recent
version\todosubst{What if there are conflicting versions?}
and compare the total number of valid signatures to the threshold $\FunEval$. If the
\KwPetition~passes, the new server set should immediately set up the
next iteration of the DIN layer.\toadd{finish describing new setup}

\section{Arguments for Correctness}
\subsection{Verifiability}
Our protocol provides all three types of verifiability specified in
Section~\ref{Section:verif}.

\begin{theorem} This protocol is Verifiable\end{theorem}

\begin{proof}

  \begin{lemma}The \StructElectionState~of any \StructElection at
  any time is well defined. \end{lemma}
  \begin{proof}This follows from properties of peer-to-peer Dissent \cite{sec}.
    The \StructElectionState~can only be updated by transmission of messages
    (votes) over Dissent. Recall that communication proceeds in serialized
    \emph{rounds}, so by Theorem~\ref{theorem:rounds}, it is impossible for two
    \KwPeer s to have conflicting versions of the election state at any
    given round.
  \end{proof}

  Given this, we know that every \KwPeer~has accurate knowledge of the
  election state if it has any knowledge of the election state. From here, the
  verifiability properties follow directly from the properties of linkable ring
  signatures.

  \todo[inline, caption={TODO: More proof detail}]{TODO: Here's more proof detail:

  \begin{lemma} Given accurate knowledge of the current election state $(\State,
    \VarPetition, \SetVotes)$, a \KwPeer can verify that its vote has been
    included or excluded correctly.
  \end{lemma}
  \begin{proof}a \KwPeer $\peer$ can call
    \NameSign($\VarManifest.\KwRoster.keys, \VarPetition.\KwLinkScope, \msg.k,
    \VarPetition$) %\todo{TODO:What's $k$?}
    to produce a
    signature $\sig$, then examine $\SetVotes$ to see if it contains $\sig$.
  \end{proof}
}

\end{proof}
    % Our protocol provides individual verifiability.
    %
    % --- this follows from the
    % properties of Dissent in Numbers and of linkable ring signatures.%: Since every
    % \paragraph{Lemma 1:} There is a well-defined state.
    %
    % \paragraph{Lemma 1:} Given accurate knowledge of the current election state
    % $(S, P, G)$, a \texttt{Member} $m$ can call
    % $m$.\textsc{Sign}($S.M.\texttt{Roster}.keys$,$P.\texttt{LinkScope}$,$m$.$k$,
    % $P$) to produce a signature $s$, then examine $G$ to see if it contains $s$.
    % By properties of linkable ring signatures,
    %
\subsection{Anonymity}
Although the voting protocols discussed in Section~\ref{Section:evoting}
provide voter anonymity (secret ballots) within an election, they do not on
their own provide instigator anonymity. This protocol provides both.

\begin{lemma} Votes are $\NumHonest$-anonymous among the $\NumHonest$ honest
  users of the system \end{lemma}
\begin{proof} This follows directly from Theorem~\ref{theorem:anon}.\end{proof}

Using this, we can show:

\begin{theorem} This protocol provides Secret Ballots \end{theorem}
\begin{proof} Anyone monitoring traffic can trivially link a vote to its Dissent
  pseudonym, but since this changes every round \cite{sec}, this provides no
  information beyond the scope of a single petition.
\end{proof}

\begin{theorem} This protocol provides Secret Instigators \end{theorem}
\begin{proof} Similarly, since the Hardened Dissent layer runs at all times,
  every participant is essentially actively submitting an anonymous petition or
  non-petition every round, and so neither intersection attacks nor traffic
  analysis can determine the identity of the instigator of any petition.
\end{proof}