Files
proofs/pulsar/reshare-preservation.tex
zeekay 4a522e0cfc rename Pulsar_M → Pulsar (drop the -M qualifier)
Pulsar is the Module-LWE threshold ML-DSA scheme; the -M qualifier
distinguished it from an older R-LWE Pulsar (now Corona) and is now
redundant. Strip it from the formal-verification tree:

  lean/Crypto/Pulsar_M/          → lean/Crypto/Pulsar/
  namespace Crypto.PulsarM       → namespace Crypto.Pulsar
  pulsar-m/ (paper directory)    → pulsar/
  Pulsar-M / PulsarM / pulsar-m  → Pulsar / pulsar in all prose

Two duplicate papers (reshare-preservation.tex + unforgeability.tex)
had a generic top-level stub AND a substantive Pulsar-M subdirectory
version. The substantive ones (the actual mechanised reductions)
replace the stubs.

PULSAR-M-SIGN-PRNG-V1 domain-separation tag → PULSAR-SIGN-PRNG-V1.
2026-05-15 15:01:22 -07:00

122 lines
5.0 KiB
TeX

%% ============================================================
%% pulsar/reshare-preservation.tex
%% ============================================================
%%
%% Public-key invariance + soundness + privacy of Pulsar reshare
%% with beacon-randomised quorum selection.
%% ============================================================
\subsection*{Pulsar reshare public-key invariance}
\begin{theorem}[Pulsar reshare preserves $\mathit{pk}$]
\label{thm:pulsar-reshare-pkinv}
Let $(\mathcal{O}, t_{\mathrm{old}})$ be the old committee and
threshold, and $(\mathcal{N}, t_{\mathrm{new}})$ be the new committee
and threshold of a Pulsar reshare against beacon $\beta_e$. Let
$\mathbf{s}'_j$ and $\mathbf{u}'_j$ be the new shares produced for
each $j \in \mathcal{N}$. For every threshold subset $T' \subseteq
\mathcal{N}$ with $|T'| = t_{\mathrm{new}}$,
\[
\sum_{j \in T'} \lambda_j^{T'} \cdot \mathbf{s}'_j \;=\; \mathbf{s}_1
\quad\text{and}\quad
\sum_{j \in T'} \lambda_j^{T'} \cdot \mathbf{u}'_j \;=\; \mathbf{u} \pmod q.
\]
Therefore the FIPS~204 public key $\mathit{pk} = (\rho, \mathbf{t}_1)$
where $\mathbf{t} = \mathbf{A} \mathbf{s}_1 + \mathbf{B} \mathbf{u}$
is invariant under reshare.
\end{theorem}
\begin{proof}
Define $G(X) = \sum_{i \in \mathcal{Q}_e} g_i(X)$ where
$\mathcal{Q}_e$ is the beacon-selected reshare quorum. $G$ has
degree at most $t_{\mathrm{new}} - 1$ and constant term
\[
G(0) \;=\; \sum_{i \in \mathcal{Q}_e} g_i(0)
\;=\; \sum_{i \in \mathcal{Q}_e} \lambda_i^{\mathcal{Q}_e} \mathbf{s}_i
\;=\; \mathbf{s}_1
\]
by Lagrange interpolation over the old quorum. The new shares are
$\mathbf{s}'_j = G(j)$ for $j \in \mathcal{N}$, so
$\{\mathbf{s}'_j\}$ are valid Shamir shares of $G(0) = \mathbf{s}_1$
with threshold $t_{\mathrm{new}}$. The same argument applies to
$\{\mathbf{u}'_j\}$. \qed
\end{proof}
\subsection*{Pulsar reshare soundness}
\begin{theorem}[Pulsar reshare soundness]
\label{thm:pulsar-reshare-sound}
For every $\PPT$ adversary $\mathcal{A}$ against RESHARE-SOUND,
\[
\mathrm{Adv}^{\mathsf{RESHARE\text{-}SOUND}}_{\mathsf{Pulsar\text{-}M}}(\mathcal{A})
\;\le\;
\mathrm{Adv}^{\mathsf{MSIS}}_{q, k, 2\ell, \beta_{\mathrm{bind}}}(\mathcal{B}).
\]
\end{theorem}
\begin{proof}
The reshare polynomials $g_i, h_i$ commit to constant terms
$\lambda_i^{\mathcal{Q}_e} \mathbf{s}_i,\,
\lambda_i^{\mathcal{Q}_e} \mathbf{u}_i$ under Pedersen commit.
Pedersen binding prevents a deviating $i \in \mathcal{Q}_e \cap
\mathcal{C}$ from substituting a different constant term. The
remaining honest parties' constant terms sum to $\mathbf{s}_1$
exactly by \Cref{thm:pulsar-reshare-pkinv}. \qed
\end{proof}
\subsection*{Pulsar reshare share privacy under beacon randomness}
\begin{theorem}[Reshare share privacy]
\label{thm:pulsar-reshare-priv}
For an unbiased beacon $\beta_e$ and up to $t-1$ corruptions per
side,
\[
\mathrm{Adv}^{\mathsf{RESHARE\text{-}PRIV}}_{\mathsf{Pulsar\text{-}M}}(\mathcal{A})
\;\le\;
\mathrm{Adv}^{\mathsf{MLWE}}_{q, k, \ell, \eta}(\mathcal{B}_{\mathrm{MLWE}})
+ \mathrm{Adv}^{\mathsf{beacon\text{-}unbias}}_{\mathrm{chain}}(\mathcal{B}_{\beta})
+ q^{-1}.
\]
\end{theorem}
\begin{proof}
The old-committee leaked shares $\{\mathbf{s}_i\}_{i \in
\mathcal{C}_{\mathrm{old}}}$ alone reveal nothing about
$\mathbf{s}_1$ by Shamir secret sharing. The new shares
$\{\mathbf{s}'_j\}_{j \in \mathcal{C}_{\mathrm{new}}}$ similarly
leak nothing on their own. The cross-leakage from the dealing step
contributes $\{g_i(j) : i \in \mathcal{Q}_e,\, j \in
\mathcal{C}_{\mathrm{new}}\}$. Conditioned on $\mathbf{s}_i$ (which
$\mathcal{A}$ already knows if $i \in \mathcal{C}_{\mathrm{old}}$,
otherwise hidden), the distribution of $g_i(j)$ for $|\{j\}| <
t_{\mathrm{new}}$ is uniform in $\Rq^\ell$ by the random high-degree
coefficients of $g_i$; the dealing-step view admits a simulator
that draws the leaked $g_i(j)$ values uniformly without knowing
$\mathbf{s}_1$.
The beacon-unbiasability assumption ensures
$\mathcal{Q}_e \cap \mathcal{C}_{\mathrm{old}}$ is a fresh uniform
sample with respect to $\mathbf{s}_1$, preventing adversarial
gaming of the quorum (the F10 weakness in Pulsar's pre-fix
deterministic reshare; addressed in DD-006 of the Pulsar
\texttt{docs/design-decisions.md}).
The $q^{-1}$ term is the negligible probability that a Lagrange
denominator collides in the beacon-induced ordering. \qed
\end{proof}
\paragraph{Forward security.}
\Cref{thm:pulsar-reshare-priv} plus \Cref{thm:pulsar-reshare-pkinv}
together imply the standard proactive-secret-sharing forward-
security property: revealing all shares at epoch $e$ leaks no
information about $\mathbf{s}_1$ in epoch $e' > e$ provided fewer
than $t-1$ parties have leaked their epoch-$e'$ shares. This is
the load-bearing property of the mobile-adversary game
(\Cref{game:mob} in \texttt{pulsar/spec/security-games.tex}).
\paragraph{Scaling.}
All three theorems in this file are independent of the committee
size $n$. The reshare-protocol security guarantees therefore
extend verbatim to the extreme committee size $N^\star =
1\,111\,111$.