Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

• URL: http://arxiv.org/abs/2604.20793v2
• Date: Sat, 25 Apr 2026 05:32:07 GMT
• Title: Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware
• Abstract summary: Post-quantum cryptographic (PQC) accelerators rely on pipelined Number Theoretic Transform stages over $mathbbZ_q$.<n>Our prior work established structural dependency analysis at scale and quantified the security margin of partial NTT masking.<n>We present three machine-checked results in Lean 4 with Mathlib, all zero sorry.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Post-quantum cryptographic (PQC) accelerators for ML-KEM (FIPS 203) and ML-DSA (FIPS 204) rely on pipelined Number Theoretic Transform (NTT) stages over $\mathbb{Z}_q$. Our prior work established structural dependency analysis at scale [1] and quantified the security margin of partial NTT masking [2]. Whether per-stage arithmetic masking guarantees pipeline-level security had no prior machine-checked answer for the r-bearing case: composition frameworks (ISW, t-SNI, PINI, DOM) were formalized exclusively for Boolean masking over $\mathrm{GF}(2)$; no proof assistant artifact addresses the NTT butterfly over $\mathbb{Z}_q$. We present three machine-checked results in Lean 4 with Mathlib, all zero sorry. First, we close a stated limitation of prior work: value-independence implies constant marginal distribution under fresh randomness (via an algebraic MutualInfoZero proxy). Second, butterfly per-context uniformity: for any Cooley-Tukey butterfly with fresh output mask over $\mathbb{Z}/q\mathbb{Z}$ ($q > 0$), each output wire has exactly one mask value producing each output, a uniform marginal independent of secrets, universal over all moduli, twiddle factors, and inputs. Third, a k-stage NTT pipeline with fresh per-stage masking satisfies per-context uniformity at every stage under the ISW first-order probing model. We document a named warning: pointwise value-independence is false for butterfly outputs. The Adams Bridge accelerator (CHIPS Alliance Caliptra) fails the fresh masking hypothesis, masking active only in INTT round 0, architecturally explaining its structural insecurity. Artifact: nine theorems, 1,738 build jobs, zero sorry. Composition for nonlinear gadgets (Barrett) is addressed in forthcoming manuscripts proving Barrett's PF-PINI(2) satisfaction (one-bit barrier) [3] and k-stage composition for PF-PINI gadgets under fresh-mask renewal [4].

Related papers

• SSTQ:Privacy-Preserving Vector Quantization via Subsampled Stochastic TurboQuant [79.24089819400126]
  Subsampled TurboQuant (SSTQ) is a framework that combines overcomplete equal-width tight frames, coordinate subsampling, and privacy-aware quantization.<n>SSTQ achieves mean squared error scaling while using only $lceil log N il + b$ bits per client, where $N = (d)$ is the frame size.<n>We also derive a surrogate privacy-aware codebook objective that reduces the codebook-dependent MSE scaling from $O(4b)$ to $O(2b)$.
  arXiv  Detail & Related papers  (2026-08-05T17:51:25Z)
• Minimax Optimal Variance-Aware Regret Bounds for Multinomial Logistic MDPs [56.28491566735463]
  Existing algorithms for episodic Markov Decision Processes yield a regret of $smashtildeO(dH2sqrtT)$.<n>We propose an algorithm achieving a regret of $smashtildeO(dH2bar_TsqrtT)$, which recovers the existing bound in the worst case and improves upon it for structured MDPs.
  arXiv  Detail & Related papers  (2026-05-19T12:39:32Z)
• The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware [0.0]
  This paper closes a series of formally-verified analyses of masked NTT hardware for post-quantum cryptography.<n> Arbitrary-depth $k$-stage masked NTT pipelines with fresh inter-stage masking and per-stage PF-PINI($leq 2$) gadgets satisfy a per-observation cardinality bound of $2 cdot q2k-2$.
  arXiv  Detail & Related papers  (2026-05-04T17:32:31Z)
• Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking [0.0]
  We prove, to our knowledge, the first machine-checked composition theorems for arithmetic masking over prime fields.<n>For two PF-PINI gadgets with parameters $k_$ and $k$, the composed two-stage pipeline with fresh masking satisfies PF-PINI($k$), Stage 1's multiplicity is completely erased from the composed output.<n>We formally bridge the algebra and hardware-faithful arithmetic models of Barrett reduction, and instantiate the theorems to diagnose Microsoft's Adams Bridge PQC accelerator.
  arXiv  Detail & Related papers  (2026-04-28T17:21:20Z)
• Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware [0.0]
  Barrett reduction is the nonlinear core of every practical NTT-based post-quantum cryptography implementation.<n>Existing composition frameworks address masking over GF(2); none provides a machine-checked characterization of Barrett's leakage.<n> PF-PINI satisfies PF-PINI(2); the Cooley-Tukey butterfly satisfies PF-PINI(1).
  arXiv  Detail & Related papers  (2026-04-27T16:27:33Z)
• From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification [0.0]
  Formal verification of masking in post-quantum cryptographic (PQC) hardware relies on SMT solvers over finite domains.<n>Our prior work established structural dependency analysis at scale and quantified the security margin of partial NTT masking.<n> QANARY, our structural dependency analysis framework, verified 1.17 million cells across 30 modules of the Adams Bridge ML-DSA/ML-KEM accelerator.
  arXiv  Detail & Related papers  (2026-04-20T18:17:22Z)
• Cryptanalysis of the Legendre Pseudorandom Function over Extension Fields [0.0]
  The Legendre Pseudorandom Function (PRF) is a highly efficient cryptographic primitive built upon the Legendre symbol.<n>Recent interest has shifted toward instantiations over extension fields $mathbbF_pr$.<n>This paper presents the first comprehensive cryptanalysis of the single-degree Legendre PRF operating over $mathbbF_pr$.
  arXiv  Detail & Related papers  (2026-04-06T16:35:32Z)
• Adaptation to Intrinsic Dependence in Diffusion Language Models [5.185131234265025]
  Diffusion language models (DLMs) have emerged as a promising alternative to autoregressive (AR) approaches.<n>We introduce a distribution-agnostic unmasking schedule for DLMs that adapts to the (unknown) dependence structure of the target data distribution.<n>Our results significantly improve upon prior convergence theories and yield substantial sampling acceleration for low-complexity distributions.
  arXiv  Detail & Related papers  (2026-02-23T18:41:34Z)
• FIPS 204-Compatible Threshold ML-DSA via Masked Lagrange Reconstruction [0.0]
  Masked Lagrange reconstruction enables threshold ML-DSA with arbitrary thresholds $T$.<n>We produce standard 3.3 KB signatures verifiable by unmodified 204 implementations.
  arXiv  Detail & Related papers  (2026-01-28T18:13:47Z)
• MaskPro: Linear-Space Probabilistic Learning for Strict (N:M)-Sparsity on Large Language Models [53.36415620647177]
  Semi-structured sparsity offers a promising solution by strategically retaining $N$ elements out of every $M$ weights.<n>Existing (N:M)-compatible approaches typically fall into two categories: rule-based layerwise greedy search, which suffers from considerable errors, and gradient-driven learning, which incurs prohibitive training costs.<n>We propose a novel linear-space probabilistic framework named MaskPro, which aims to learn a prior categorical distribution for every $M$ consecutive weights and subsequently leverages this distribution to generate the (N:M)-sparsity throughout an $N$-way sampling
  arXiv  Detail & Related papers  (2025-06-15T15:02:59Z)
• Learning with Norm Constrained, Over-parameterized, Two-layer Neural Networks [54.177130905659155]
  Recent studies show that a reproducing kernel Hilbert space (RKHS) is not a suitable space to model functions by neural networks. In this paper, we study a suitable function space for over- parameterized two-layer neural networks with bounded norms.
  arXiv  Detail & Related papers  (2024-04-29T15:04:07Z)
• Communication-Constrained Bandits under Additive Gaussian Noise [111.06688156723018]
  We study a distributed multi-armed bandit where a client supplies the learner with communication-constrained feedback. We propose a multi-phase bandit algorithm, $mathttUEtext-UCB++$, which matches this lower bound to a minor additive factor.
  arXiv  Detail & Related papers  (2023-04-25T09:31:20Z)
• Minimax-Optimal Multi-Agent RL in Zero-Sum Markov Games With a Generative Model [50.38446482252857]
  Two-player zero-sum Markov games are arguably the most basic setting in multi-agent reinforcement learning. We develop a learning algorithm that learns an $varepsilon$-approximate Markov NE policy using $$ widetildeObigg. We derive a refined regret bound for FTRL that makes explicit the role of variance-type quantities.
  arXiv  Detail & Related papers  (2022-08-22T17:24:55Z)
• BRST-BV Quantum Actions for Constrained Totally-Symmetric Integer HS Fields [77.34726150561087]
  A non-minimal constrained BRST-BV Lagrangian formulation is presented for totally symmetric massless HS fields in a $d$-dimensional Minkowski space. A Fock-space quantum action is constructed as a shift of the total generalized field-antifield vector by a variational derivative of the gauge-fixing Fermion $Psi$ in a total BRST-BV action.
  arXiv  Detail & Related papers  (2020-10-29T16:40:32Z)
• Provably Efficient Safe Exploration via Primal-Dual Policy Optimization [105.7510838453122]
  We study the Safe Reinforcement Learning (SRL) problem using the Constrained Markov Decision Process (CMDP) formulation. We present an provably efficient online policy optimization algorithm for CMDP with safe exploration in the function approximation setting.
  arXiv  Detail & Related papers  (2020-03-01T17:47:03Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.