mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
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.
122 lines
5.0 KiB
TeX
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$.
|