Formalize and prove crocus

paper/Makefile

@@ -18,6 +18,7 @@ SRC+= 	protest-model.tex
 SRC+= 	verifiability-properties.tex
 SRC+=	privacy-properties.tex
 SRC+= 	adversary-model.tex 
+SRC+= 	formalization.tex
 SRC+= 	building-blocks.tex
 SRC+= 	ZKPK.tex
 #SRC+= 	ZKPK-instantiations.tex

paper/contents.tex

@@ -12,6 +12,7 @@
 \include*{system-model}
 \include*{related-work}
 \include*{definitions}
+\include*{formalization}
 \include*{building-blocks}
 %\include*{DB-anon-cred}
 \include*{protocol}

paper/formalization.tex

@@ -0,0 +1,268 @@
+\section{Formalization}
+
+\subsection{Setup}
+
+\emph{Setup: \((\spk, \ssk)\gets \CROCUSsetup\).}
+Generates a service public--private key-pair~\((\spk, \ssk)\).
+
+\emph{Registration: \(\sk\gets 
+    \Proto{\CROCUSreg[_P][\spk]}{\CROCUSreg[_{\CA}][\ssk]}\).}
+An interactive protocol which returns the secret key~\(\sk\) of the 
+participant~\(P\).
+
+\subsection{Participation}%
+\label{ProtocolDuring}
+
+\emph{Creation of a protest: \(\cid\gets \GenProtest[s]\).}
+Takes a string~\(s\in\{0,1\}^*\) describing the protest cause and returns a 
+unique cause identifier~\(\cid\).
+
+\emph{Joining: \((\pid, t_s)\gets \CROCUSjoin[_P][\cid]\).}
+Takes the cause identifier~\(\cid\) of a protest and returns the protester' 
+protest-specific identifier~\(\pid\) along with a time-stamp~\(t_s\).
+
+A protester who wants to join the protest uses the manifesto to
+compute an identifier for the cause by hashing the manifesto,
+\(\cid\gets \Hash[\mfst]\) (and comparing the result to that received
+from the organizer, we omit this in the protocol for readibility).
+Afterwards, this identifier is used to create the protest-specific identifier 
+for the protester, \(\pid\gets \ACprf[_{\sk_P}][\cid]\)%
+% (see \cref{fig:ProofFig} and \cref{ACprfAlg} in the appendix for details of 
+%the algorithms)%
+.
+The protester also fetches a time-correlated random value, \(t_s\), from 
+\(\TS\), \(t_s\gets \TSget\).
+
+
+\emph{Joining as a witness: \(t_s'\gets \CROCUSjoin_W\).}
+The witness simply gets a time-correlated random value from the time-stamping service, \(t_s'\gets \TSget\).
+Note that we do this for redundancy, the newest of \(t_s\) and \(t_s'\) will 
+set the start of the time interval of creation for the proof share.
+
+
+\emph{Participation: \(\pi\gets
+    \Proto{\CROCUSparticipate[\cid, \sk_P]}{\CROCUSwitness[\sk_W, \spk]}\),}
+In the participation phase, the protester and 
+the witness construct the proof share of the protester (\cref{fig:ProofFig}).
+
+The protester sends \(\pid\) and \(t_s\) to the witness.
+Then they run the protocol \[
+  \Proto{\ACproveSig[\spk, k, r, \sigma]}{\ACverifySig[\spk, \ssk]}
+\] (see \cref{ACacAlg}), \(k\) and \(r\) are part of \(\sk_P\).
+Note that the \acf{PK} in \cref{ACacAlg} must be
+run as a \iacf{PPK}, which we do by distance bounding.
+If the protocol succeeds, the witness will compute \(\wid \gets 
+  \ACprf[_{\sk_W}][\pid]\) and send \((\wid, t_s', l)\) to the protester.
+
+
+\emph{Submission: \(\psh_P\gets \CROCUSsubmit[_P][\cid, \pid, \wid, t_s, t_s',  l]\).}
+The protester commits the proof-share data to the ledger~\(L\) and receives the 
+proof of commitment, \(t_e\gets \TSsubmit[\Hash[\cid, \pid, \wid, t_s, t_s', 
+  l]]\).
+The sooner this is done, the higher the precision for the time-dependent 
+eligibility criterion will be for later counting.
+The remaining operations are not time critical.
+
+The protester computes \iac{NIZK} proof \(\corr_{\pid}\), which shows the 
+correctness of \(\pid\).
+More specifically,
+\begin{multline*}
+  \corr_{\pid}\gets \SPK\left\{ (\sk_P) : \right. \\
+    \begin{aligned}
+      \pid &= \ACprf[_{\sk_P}][\cid] \quad \land \\
+      \sigma_P' &= \left. \ACblind[\ACsign[_{\ssk}][\sk_P]] \right\}
+    \end{aligned} \\
+      (\cid, \pid, \wid, t_s, t_s', l).
+\end{multline*}
+Finally, the protester uploads the tuple \[
+  \psh_P = (\cid, \pid, \wid, t_s, t_s', t_e, l, \corr_{\pid})
+\] for permanent storage, \(\TSsubmit[\psh_P]\).
+
+\emph{Submission: \(\psh_W\gets \CROCUSsubmit[_W][\cid, \pid, \wid, t_s, t_s', 
+    l]\).}
+The witness, like the protester, commits the proof-share data to the 
+ledger, \(t_e\gets \TSsubmit[\Hash[\cid, \pid, \wid, t_s, t_s', l]]\).
+%(This is to make the time interval as early as possible, whoever is the faster 
+%will submit it.) \sonja{but both do}
+Then, without any time requirements, the witness computes \iac{NIZK} proof 
+\(\corr_{\wid}\) as follows:
+\begin{multline*}
+  \corr_{\wid}\gets \SPK\left\{ (\sk_W) : \right. \\
+    \begin{aligned}
+      \wid &= \ACprf[_{\sk_W}][\pid] \quad \land \\
+      \sigma_W' &= \left. \ACblind[\ACsign[_{\ssk}][\sk_W]] \right\}
+    \end{aligned} \\
+      (\cid, \pid, \wid, t_s, t_s', l).
+\end{multline*}
+Finally, the witness uploads the tuple \[
+  \psh_W = (\cid, \pid, \wid, t_s, t_s', t_e', l, \corr_{\wid})
+\] for permanent storage on the ledger, \(\TSsubmit[\psh_W]\).
+
+
+\begin{figure*}
+  \centering
+  \small
+  \begin{subfigure}{\columnwidth}
+    \begin{align*}
+      O\to \text{all}\colon & \text{manifesto} \\
+      P\colon & t_s\gets \TSget \\
+        & \cid\gets \Hash[\text{manifesto}], \\
+        & \pid\gets \ACprf[_{\sk_P}][\cid] \\
+      W\colon & t_s'\gets \TSget
+      \\[-1em]
+      \noalign{\hfill Join}
+      \midrule
+      \noalign{\hfill Participation}
+      \\[-3em]
+      P\to W\colon & \pid \\
+      P\leftrightarrow W\colon &
+        \PPK\mleft\{ (\sk_P) : \mright. \\
+        & \qquad \pid = \ACprf[_{\sk_P}][\cid], \\
+        & \qquad \mleft. \sigma_P' = \ACblind[\ACsign[_{\ssk}][\sk_P]] \mright\} 
+        \\
+      W\colon & \wid\gets \ACprf[_{\sk_W}][\pid] \\
+      W\to P\colon & (\wid, t_s', l)
+    \end{align*}
+    \caption{Join and participation.}
+  \end{subfigure}
+  \hfill
+  \begin{subfigure}{\columnwidth}
+    \begin{align*}
+      P\colon & t_e\gets \TSsubmit[\Hash[\pid, \wid, t_s, t_s', l]] \\
+      W\colon & t_e'\gets \TSsubmit[\Hash[\pid, \wid, t_s, t_s', l]] \\
+      W\colon & \TSsubmit[(\cid, \pid, \wid, t_s, t_s', t_e, l, 
+      \pi_{\wid})],\quad \text{where} \\
+        & \pi_{\wid} = \SPK\mleft\{ (\sk_W) : \mright. \\
+        & \qquad \wid = \ACprf[_{\sk_W}][\pid], \\
+        & \qquad \mleft. \sigma_W' = \ACblind[\ACsign[_{\ssk}][\sk_W]]\mright\} 
+        \\
+        & \qquad\qquad (\cid, \pid, \wid, t_s, t_s', l) \\
+      P\colon & \TSsubmit[(\cid, \pid, \wid, t_s, t_s', t_e, l, 
+      \pi_{\pid})],\quad \text{where}\\
+        & \pi_{\pid} = \SPK\mleft\{ (\sk_P) : \mright. \\
+        & \qquad \pid = \ACprf[_{\sk_P}][\cid], \\
+        & \qquad \mleft. \sigma_P' = \ACblind[\ACsign[_{\ssk}][\sk_P]] \mright\} 
+        \\
+        & \qquad\qquad (\cid, \pid, \wid, t_s, t_s', l)
+    \end{align*}
+    \caption{Submission.}
+  \end{subfigure}
+  \caption{%
+    An overview of \CROCUS participation.\@
+    The organizer \(O\) broadcasts the manifesto.
+    The protester \(P\), witness \(W\) and their computations are as in \cref{fig:ProofFig}.
+    Finally, both \(P\) and \(W\) submit the proof shares to a
+   public ledger for permanent storage \(S\). Note that \pid  always refers to the
+    protester whose presence is being witnessed.
+  }%
+  \label{fig:ProtocolOverview}
+\end{figure*}
+%\normalsize
+
+
+\subsection{Count and Verification}%
+\label{ProtocolVerification}
+
+% While there are various ways for verifying the participation count, hereafter, 
+% we will detail the two suggested just after \cref{DefParticipationCount}.
+% In the first approach, we do not trust individual witnesses, rather we \emph{assume} that it is difficult for Alice to find more than \(\theta\) witnesses willing to collude.
+% Thus, the strength comes from the number of witnesses and we require at least \(\theta\) witnesses to accept a participation proof as valid.
+% In the second approach, we trust specific witnesses, but no others.
+% In this case, to accept a participation proof as valid, we require at least one trusted witness, the independent journalist Jane.
+% It is the strength function \(\str\) of \cref{DefParticipationCount} that 
+% differ in the two cases.
+% We will first give the procedure and then how to construct the two different 
+% strength functions.
+
+
+To count or verify the participation count for a protest \(\prtst\) with 
+identifier \(\cid_0\), a verifier must download the set \(\pshs_{\cid_0}\) of 
+all \(s_P\) and \(s_W\) tuples containing \(\cid_0\) from the ledger~\(\TS\).
+Then from \(\pshs_{\cid_0}\), a verifier can build, in succession,
+\begin{enumerate*}
+\item the valid proof shares \(s_j^{(i)}\) for all matching pairs \((s_P, 
+    s_W)\) corresponding to a witness \(i\) and a protester \(j\),
+\item the participation proof \(\prf_{j}\) for each protester \(j\),
+\item the set \(\prfs_{\prtst}^{\str,\theta}\) of eligible participation proofs 
+  for all protesters in \(\prtst\), and finally,
+\item the participation count, \ie the cardinality of 
+  \(\prfs_\prtst^{\str,\theta}\).
+\end{enumerate*}
+
+More precisely, given \[
+  \pshs_{\cid_0} = \{ (\cid, \pid, \wid, l, t_s, t_s', t_c, \corr) \in \pshs 
+  \mid \cid = \cid_0 \}
+\] and a matching pair \((s_P, s_W) \in {\pshs_{\cid_0}}^2\) for a witness 
+\(i\) and a protester \(j\) with
+\begin{align*}
+  s_P &= (\cid_0, \pid_j, \wid_i, l, t_s, t_s', t_c, \corr_i) &\text{and} \\
+  s_W &= (\cid_0, \pid_j, \wid_i, l, t_s, t_s', t_c', \corr_j),
+\end{align*}
+%, with matching values for \(cid_0, pid_j, wid_i, l, t_s, t_s'\),
+the verifier can build a valid proof share \(s_j^{(i)}\) certified by \(i\) for 
+\(j\) as follows:
+verify \(\corr_i\) and \(\corr_j\),
+let
+\begin{align*}
+  t &= \interval{\max(t_s, t_s')}{\min(t_c, t_c')} &\text{and} \\
+  s_j^{(i)} &= (\cid_0, \pid_j, \wid_i, l, t),
+\end{align*}
+as in \cref{DefProofShare},
+check that \(s_j^{(i)}\) is valid (\ie happened during and at the location of 
+the protest), as in \cref{DefProofShare}.
+
+Then the set of all valid proof shares for a protester \(j\) constitutes its 
+participation proof \(\prf_{j}\), as in \cref{DefParticipationProof},
+and the verifier thus can derive the set of \((\str,\theta)\)-eligible participation proofs \(\prfs_{\prtst}^{\str,\theta}\) for all protesters for the protest \(\prtst\), as in \cref{DefParticipationCount}.
+Finally, the  participation count \(|\prfs_{\prtst}^{\str,\theta}|\) is the cardinality of this set by  \cref{DefParticipationCount}.
+
+
+% MOST PROBABLY obsolete below v 
+
+%To verify the participation count for a protest \(\prtst\)  with identifier $\cid$
+%(see \cref{DefProtest}), a verifier must download all the proof shares \[
+%  \psh_i =   (\cid, \pid_j, \wid_i, t_s^{(i)}, t_s^{\prime (i)}, t_e^{(i)}, 
+%  t_e^{\prime   (i)}, l_i, \corr_{\pid_j}^{(i)}, \corr_{\wid_i})
+%\] for each protester \(j\) from the ledger, verify \(\corr_{\pid_j}^{(i)}\), 
+%\(\corr_{\wid_i}\) and that the interval \(\interval{\max(t_s^{(i)}, 
+%    t_s^{\prime (i)})}{\min(t_e^{(i)}, t_e^{\prime (i)})}\subseteq t\) and that 
+%\(l_i\subseteq  l\).
+%Any proof share that does not verify correctly will be discarded.
+%At this point, the verifier has constructed the set \(S\) from 
+%\cref{DefProofShares} and can thus construct any participation proof 
+%\(\prf_{\pid_j, P}\) as in \cref{DefParticipationProof}.
+%Now the verifier can compute the participation count \(|\prfs_P^{\str, 
+%    \theta}|\) as in \cref{DefParticipationCount}.
+
+
+%__________________________
+
+% In the case \emph{without} trusted witnesses, all the weights equal to 1 is equivalent to counting the elements in the set, 
+% \(\str[\prf_{\pid_j, P}] = |\prf_{\pid_j, P}|\).
+
+In the case of trusted witnesses, each such trusted witness must
+publish or otherwise inform the verifier of which proof shares they
+have signed, \eg by giving a list of all such proof shares or
+digitally signing each proof share\footnote{%
+  To achieve witness privacy in this situation, one could employ a
+  group or ring signature scheme for a set of potentially trusted witnesses, \eg
+  members of an independent journalist association.  Then one learns
+  that at least one member of this set must have
+  been there.
+}.
+
+Note that, thanks to the \((\str,\theta)\)-eligibility criterion
+(\cref{DefParticipationCount}), the method of counting is extremely
+generic, and each (counting) verifier can make an independent choice to regulate their trust in the final result, based on their initial trust in the witnesses. In other words, anyone who does the counting can choose the eligibility
+criteria (time interval, location, number of regular or trusted
+witnesses, who is considered to be a trusted witness) for their own count
+and as long as these are published along with the result, anyone can
+verify the correctness of the count under those criteria, and potentially question the validity of this choice. Biased or partisan verifiers may be tempted to make extreme choices, but they will have to publish those choices and lose credibility. Reasonable verifiers on the other hand will try to find a good middle-ground that counts all legitimate protesters while being resistant to isolated malicious agents.
+
+% Then the verifier can define \[
+%   \str[\prf_{\pid_j, P}] = \begin{cases}
+%     1 & \text{if \(\exists \psh_i\in \prf_{\pid_j, P}\) that is such a proof 
+%       share} \\
+%     0 & \text{otherwise}
+%   \end{cases}
+% \] and sets \(\theta = 1\).

paper/preamble.tex

@@ -113,6 +113,7 @@
 \NewVariable{\sk}{sk}
 \NewVariable{\spk}{spk}
 \NewVariable{\ssk}{ssk}
+\NewAlgorithm{\GenProtest}{GenProtest}
 \NewAlgorithm{\CROCUSreg}{Reg}
 \NewAlgorithm{\CROCUSjoin}{Join}
 \NewVariable{\mfst}{manifesto}