From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

• URL: http://arxiv.org/abs/2604.18717v2
• Date: Wed, 22 Apr 2026 17:58:06 GMT
• Title: From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification
• Abstract summary: 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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal verification of masking in post-quantum cryptographic (PQC) hardware relies on SMT solvers over finite domains. Our prior work established structural dependency analysis at scale [1] and quantified the security margin of partial NTT masking [2]. QANARY, our structural dependency analysis framework, verified 1.17 million cells across 30 modules of the Adams Bridge ML-DSA/ML-KEM accelerator [3, 4], but its core soundness result (Theorem 3.9.1) was machine-checked only at $q = 5$ via $2^{25}$ Boolean wire functions. This left portability to ML-KEM ($q = 3{,}329$, FIPS 203 [5]) and ML-DSA ($q = 8{,}380{,}417$, FIPS 204 [6]) as an open gap. NIST IR 8547 [7] (March 2025) motivates closing such gaps. We present the first machine-checked universal proof of the $r$-free sub-theorem of Theorem 3.9.1: for every $q > 0$, every wire function, and every pair of secrets, value-independence implies identical marginal distributions. The proof, in Lean 4 [8] with Mathlib [9], requires five lines versus $2^{25}$ finite evaluations. It is sorry-free, reducing the trusted base from {Z3 [10], CVC5 [11], Python} to the Lean 4 kernel. We provide nine theorems (T1--T6, T1', T3') covering reparametrization, bijectivity, overflow bounds, RNG bias, and a universal non-tightness counterexample for all $q \geq 2$. The results establish commutative ring axioms of $\mathbb{Z}/q\mathbb{Z}$ as the natural abstraction layer for arithmetic masking verification.

Related papers

• The I3322 quantum value is attained spatially but not in finite dimension [0.0]
  Let $S$ be the quantum supremum of the $I_3322$ Bell functional in the Collins-Gisin normalization (classical bound 0; two-qubit maximum exactly 1/4)<n>We prove: (i) no finite-dimensional quantum strategy attains $S$ -- any finite local dimensions, pure or mixed states, projective or POVM measurements -- proving Pal and Vertesi (2010)<n>We also determine the dimension complexity: with $S_d$ the optimum at local dimension $le d$ and $D()=mind:S-S_d
  arXiv  Detail & Related papers  (2026-09-03T15:48:01Z)
• A phase transition in the exactness of the NPA hierarchy at the critical doubly-tilted CHSH functional [0.0]
  We prove the exact quantum maximum of the doubly-tilted CHSH functional $B_=langle A_0rangle+l B_0rangle+mathrmCHSH$.<n>For all $,ge 1$ and every level the hierarchy is exact, via three explicit rational certificates realizing an affine identity.<n>On the subcritical side we certify the first four levels in exact arithmetic.
  arXiv  Detail & Related papers  (2026-07-15T12:34:25Z)
• Imbuing Large Language Models with Bidirectional Logic for Robust Chain Repair [44.80087038178069]
  We introduce Teleological Reasoning Infilling (TRI), a training framework that endows decoder-only transformers with a native emphgoal-conditioned bridging capability.<n>At inference, TRI operates as a surgical repair module within a dual-system loop.<n>Experiments on three benchmarks demonstrate that TRI achieves state-of-the-art performance across all tasks, while reducing per-problem token expenditure by 31.2%.
  arXiv  Detail & Related papers  (2026-06-03T15:58:48Z)
• Module Lattice Security (Part IV): Probabilistic Polynomial Quantum Attack on Module-LWE over 2-Power Cyclotomics [1.0152838128195467]
  We present a quantum attack on ML-KEM and related 2-power cyclotomic lattice schemes.<n>We verify the resulting approximation factor satisfies $le 21 q/2=1664.5$ for ML-KEM-1024.<n>We extend the analysis to Falcon, Hawk, and NTRU over 2-power cyclotomic rings with quantum algorithms.
  arXiv  Detail & Related papers  (2026-05-17T12:16:04Z)
• The Collapse of Unentangled Stoquastic Merlin-Arthur Proof Systems [46.657699628769336]
  Entanglement and interference are among the most fundamental properties of quantum mechanics.<n>We prove that entanglement gives no additional power to stoquastic verification.
  arXiv  Detail & Related papers  (2026-05-15T17:52:33Z)
• What Do EEG Foundation Models Capture from Human Brain Signals? [64.48249643001402]
  Modern EEG foundation models learn directly from raw signals via self-supervised pretraining.<n>We decompose into three sub-questions: emphwhat does the model learn, emphwhat does the model use, and emphhow much can be explained<n>The audit covers three foundation models (CSBrain, CBraMod, LaBraM), five clinical tasks (MDD, Stress, ISRUC-Sleep, TUSL, Siena), and a 6-family 63-feature lexicon.
  arXiv  Detail & Related papers  (2026-05-12T01:57:53Z)
• 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)
• Optimal Scalar Quantization for Matrix Multiplication: Closed-Form Density and Phase Transition [50.36362492608702]
  We study entrywise scalar quantization of two matrices prior to multiplication.<n>We obtain a closed-form optimal point density [ star(u) propto exp!left(-fracu26right)bigl( (1-2)+2u22bigr), qquad u=fracx_X,, and prove a correlation-driven phase transition.
  arXiv  Detail & Related papers  (2026-03-20T01:53:44Z)
• Rényi exponent landscape of multipartite entanglement in free-fermion systems [51.56484100374058]
  We show that the Rényi tripartite information $I_3() exhibits a qualitatively $exclusion-dependent scaling at small Fermi momentum.<n>A direct consequence is a replica obstruction: $I_m(n)/I_m(1) sim zm-1 to 0$ for all integer $n geq 2$, so the leading von Neumann signal cannot be reconstructed from integer Rényi data.
  arXiv  Detail & Related papers  (2026-03-09T22:27:00Z)
• The Spectral Dimension of NTKs is Constant: A Theory of Implicit Regularization, Finite-Width Stability, and Scalable Estimation [0.0]
  We prove a constant-limit law $lim_ntoinfty mathbbE[r_texteff(K_n)] = mathbbE[k(x, x)]2.<n>We further establish finite-width stability: if the finite-width NTK deviates in operator norm by $O_p(m-1/2)$, then $r_texteff$ changes by $O_p(m-1/2)$.<n>We design a scalable estimator using random
  arXiv  Detail & Related papers  (2025-11-30T12:14:21Z)
• Algebraic Obstructions and the Collapse of Elementary Structure in the Kronecker Problem [0.0]
  No explicit closed-form formulas have been obtained for genuinely three-row cases in the 87 years since Murnaghan's foundational work.<n>We derive five explicit formulas for staircase-hook coefficients, and verify Saxl's conjecture for 132 three-row partitions.<n>We develop integer forcing, a proof technique exploiting the tension between continuous obstructions and discrete integrality.
  arXiv  Detail & Related papers  (2025-11-28T03:21:01Z)
• Clifford quantum cellular automata from topological quantum field theories and invertible subalgebras [10.600087006666332]
  We present a framework for constructing quantum cellular automata (QCA) from topological quantum field theories (TQFT) and invertible subalgebras (ISA)<n>This approach explicitly realizes all $mathbbZ$ and $mathbbZ_p$ Clifford QCAs in all admissible dimensions.
  arXiv  Detail & Related papers  (2025-09-08T18:00:13Z)
• Quantum-Resistant RSA Modulus Decomposition via Adaptive Rényi Entropy Optimization [0.0]
  This paper explores a theoretical approach to enhance RSA's resistance against quantum attacks.<n>We develop a framework where primes are generated with controlled proximity.<n>Main contributions include establishing a connection between prime distribution properties and quantum attack complexity.
  arXiv  Detail & Related papers  (2025-07-04T11:18:34Z)
• A Unified Framework for Uniform Signal Recovery in Nonlinear Generative Compressed Sensing [68.80803866919123]
  Under nonlinear measurements, most prior results are non-uniform, i.e., they hold with high probability for a fixed $mathbfx*$ rather than for all $mathbfx*$ simultaneously. Our framework accommodates GCS with 1-bit/uniformly quantized observations and single index models as canonical examples. We also develop a concentration inequality that produces tighter bounds for product processes whose index sets have low metric entropy.
  arXiv  Detail & Related papers  (2023-09-25T17:54:19Z)
• Average-Case Complexity of Tensor Decomposition for Low-Degree Polynomials [93.59919600451487]
  "Statistical-computational gaps" occur in many statistical inference tasks. We consider a model for random order-3 decomposition where one component is slightly larger in norm than the rest. We show that tensor entries can accurately estimate the largest component when $ll n3/2$ but fail to do so when $rgg n3/2$.
  arXiv  Detail & Related papers  (2022-11-10T00:40:37Z)
• Learning a Single Neuron with Adversarial Label Noise via Gradient Descent [50.659479930171585]
  We study a function of the form $mathbfxmapstosigma(mathbfwcdotmathbfx)$ for monotone activations. The goal of the learner is to output a hypothesis vector $mathbfw$ that $F(mathbbw)=C, epsilon$ with high probability.
  arXiv  Detail & Related papers  (2022-06-17T17:55:43Z)
• Two-way kernel matrix puncturing: towards resource-efficient PCA and spectral clustering [43.50783459690612]
  The method consists in randomly "puncturing" both the data matrix $XinmathbbCptimes n$ and its corresponding kernel (Gram) matrix $K$ through Bernoulli masks. We empirically confirm on GAN-generated image databases, that it is possible to drastically puncture the data, thereby providing possibly huge computational and storage gains.
  arXiv  Detail & Related papers  (2021-02-24T14:01:58Z)

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.