Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

• URL: http://arxiv.org/abs/2604.24670v2
• Date: Tue, 28 Apr 2026 17:48:59 GMT
• Title: Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware
• Abstract summary: 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).
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Barrett reduction is the nonlinear core of every practical NTT-based post-quantum cryptography implementation. Existing composition frameworks (ISW, t-SNI, PINI, DOM) address Boolean masking over GF(2); none provides a machine-checked characterization of Barrett's leakage under first-order arithmetic masking and the first-order probing model over prime fields. Building on our prior series, QANARY [15], partial-NTT-masking margins [14], algebraic foundations [16], and butterfly composition [18], we close this gap. We prove a trichotomy: for any $q > 0$ and shift $s$, the Barrett internal wire map $f_x(m) = ((x + 2^s - m) \bmod 2^s) \bmod q$ has preimage cardinality in $\{0, 1, 2\}$, never more. We call this the 1-Bit Barrier: max-multiplicity 2 implies at most 1 bit of min-entropy loss per internal wire, universal over all moduli. The count-zero cases, unreachable output values, reveal that actual leakage is often strictly less than 1 bit, making the bound conservative. We introduce PF-PINI (Prime-Field PINI): Barrett satisfies PF-PINI(2); the Cooley-Tukey butterfly satisfies PF-PINI(1). We observe (not yet proved) that with fresh inter-stage masking, the composed pipeline has max-multiplicity $\max(k_1, k_2)$, so the 1-Bit Barrier propagates. The trichotomy, the PF-PINI instantiations, and cardinality results are machine-checked in Lean 4 with Mathlib: 12 proved results, zero sorry, universal over all $q > 0$ (the min-entropy bound follows by standard definitions). Adams Bridge lacks fresh inter-stage masking, violating PF-PINI composition and explaining why Papers 1 [15] and 2 [14] found vulnerabilities. NIST IR 8547 recommends formal methods for PQC implementation validation. The 1-Bit Barrier provides the first universal machine-checked cardinality bound for masked Barrett reduction in ML-KEM (FIPS 203) and ML-DSA (FIPS 204), with a corresponding 1-bit leakage interpretation.

Related papers

• A Sharp Barrier for Consistent Submodular Maximization: Any Improvement over $2-\sqrt{2}$ Entails Exponential Queries or Linear Recourse [50.69285844345291]
  We study tradeoff between solution quality and stability when elements arrive over time.<n>Our algorithm has a future implementation for rational oracle$ with $O(varepsilon-1)$ recourse and separate the existence of universal-price certificates from their efficient algorithms.
  arXiv  Detail & Related papers  (2026-09-09T10:13:43Z)
• Adversarial Resilience of Poisson-Process Submodular Maximization over Matroids: From Robust Offline Optimization to Full-Bandit Learning [55.29259818039367]
  We study the nonnegative submodular subject to a general matroid when the offline algorithm is given an arbitrary controlled value oracle.<n>Our algorithm retains limiting approximation factors $1/e$ for non-monotone objectives and $1-1/e$ for monotone objectives.<n>As a consequence, the offline-to-online reduction yields single-bandit CMAB algorithms for general matroid-constrained submodular rewards.
  arXiv  Detail & Related papers  (2026-08-12T14:54:15Z)
• The Security Budget of Code-LLM Prompt Hardening: Provable Limits Under Pass-Only Acceptance [0.0]
  We operationalize the floor as the emphTri-Audit Protocol, a two-axis reporting protocol that separates a prompt-side deductive registry attribute from a model-side empirical corollary.<n>A constrained best-of-family search over deterministic and guarded learned filters on CodeLlama-7B, Qwen2.5-Coder-7B/1.5B and DeepSeek-Coder-6.7B at $n=164$ yields the emphCross-Model Tri-Audit Invariance: of twenty-eight pass-preserving rows, twelve-changed-of-record learned-can
  arXiv  Detail & Related papers  (2026-06-02T08:22:14Z)
• 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)
• Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware [0.0]
  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.
  arXiv  Detail & Related papers  (2026-04-22T17:19:22Z)
• 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)
• Fair Decoder Baselines and Rigorous Finite-Size Scaling for Bivariate Bicycle Codes on the Quantum Erasure Channel [0.14323566945483496]
  We run both uninformed and empherasure-aware surface code baselines alongside BP-OSD decoding of BB codes.<n>With standard depolarizing-weight MWPM and no erasure information, performance matches random guessing on the erasure channel.<n>BB at $N=1296$ has a modest edge in threshold over the surface code at twice the qubit count, and a 12$times$ lower normalized overhead.
  arXiv  Detail & Related papers  (2026-03-19T15:53:51Z)
• Hardness of High-Dimensional Linear Classification [58.29089693778071]
  We establish new exponential in dimension lower bounds for the Maximum Halfspace Discrepancy problem.<n>Both are fundamental problems in computational geometry and machine learning in their exact and approximate forms.
  arXiv  Detail & Related papers  (2026-03-19T15:53:41Z)
• A lower bound on the space overhead of fault-tolerant quantum computation [51.723084600243716]
  The threshold theorem is a fundamental result in the theory of fault-tolerant quantum computation. We prove an exponential upper bound on the maximal length of fault-tolerant quantum computation with amplitude noise.
  arXiv  Detail & Related papers  (2022-01-31T22:19:49Z)
• 1$\times$N Block Pattern for Network Sparsity [90.43191747596491]
  We propose one novel concept of $1times N$ block sparsity pattern (block pruning) to break this limitation. Our pattern obtains about 3.0% improvements over filter pruning in the top-1 accuracy of MobileNet-V2. It also obtains 56.04ms inference savings on Cortex-A7 CPU over weight pruning.
  arXiv  Detail & Related papers  (2021-05-31T05:50:33Z)
• 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)

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.