Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

• URL: http://arxiv.org/abs/2604.25878v2
• Date: Tue, 05 May 2026 20:59:41 GMT
• Title: Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking
• Abstract summary: 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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This is Paper 6 of a series of formally-verified analyses of masked NTT hardware for post-quantum cryptography; Paper 1 [1] established structural dependency analysis of the QANARY platform, and Paper 2 [2] quantified security margins under partial NTT masking. Boolean masking composition is well-understood through NI, SNI, and PINI. Arithmetic masking over $\mathbb{Z}_q$ for prime $q$, the foundation of NTT-based post-quantum cryptography, has lacked an analogous theory. We prove, to our knowledge, the first machine-checked composition theorems for arithmetic masking over prime fields. Our key insight is the renewal argument: when a fresh random mask is applied between two pipeline stages, the intermediate wire becomes perfectly uniform regardless of Stage 1's security parameter. For two PF-PINI gadgets with parameters $k_1$ and $k_2$, the composed two-stage pipeline with fresh masking satisfies PF-PINI($k_2$), Stage 1's multiplicity is completely erased from the composed output. Without fresh masking, intermediate wires have multiplicity up to $k_1$, creating a necessary condition for differential power analysis. We formalize both theorems in Lean 4 with 18 machine-checked proofs and zero sorry stubs. We formally bridge the algebraic and hardware-faithful arithmetic models of Barrett reduction, and instantiate the theorems to formally diagnose Microsoft's Adams Bridge PQC accelerator: its absence of fresh inter-stage masking leaves Barrett output wires non-uniform under the first-order probing model, the same architectural flaw that two independent empirical analyses [3, 4] and our own prior structural analysis [1] identified. Computational evidence further suggests the 1-Bit Barrier is universal across Barrett and Montgomery reductions.

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)
• Transformers Provably Learn to Internalize Chain-of-Thought [65.41010769606844]
  Implicit Chain-of-Thought (ICoT) trains models to internalize intermediate steps within their hidden states.<n>Log-ICoT removes thinking tokens one at a time, reducing the number of stages from linear in $k$ to logarithmic.<n>Experiments on multi-layer transformers confirm the theory and visualize how reasoning is progressively absorbed into deeper layers.
  arXiv  Detail & Related papers  (2026-05-27T15:17:06Z)
• Optimal Quantum Differential Privacy via Fisher Information Spectral Analysis [0.0]
  Quantum Fisher Information (QFI) metric governs a fundamental duality.<n>We exploit this duality to establish a geometry-aware framework for quantum differential privacy.
  arXiv  Detail & Related papers  (2026-05-22T19:36:42Z)
• 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)
• 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)
• 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)
• Cloning Games, Black Holes and Cryptography [50.022147589030304]
  We introduce a new toolkit for analyzing cloning games.<n>This framework allows us to analyze a new cloning game based on binary phase states.<n>We show that the binary phase variantally optimal bound offers quantitative insights into information scrambling in idealized models of black holes.
  arXiv  Detail & Related papers  (2024-11-07T14:09:32Z)
• The Power of Unentangled Quantum Proofs with Non-negative Amplitudes [55.90795112399611]
  We study the power of unentangled quantum proofs with non-negative amplitudes, a class which we denote $textQMA+(2)$. In particular, we design global protocols for small set expansion, unique games, and PCP verification. We show that QMA(2) is equal to $textQMA+(2)$ provided the gap of the latter is a sufficiently large constant.
  arXiv  Detail & Related papers  (2024-02-29T01:35:46Z)
• On sampling determinantal and Pfaffian point processes on a quantum computer [49.1574468325115]
  DPPs were introduced by Macchi as a model in quantum optics the 1970s. Most applications require sampling from a DPP, and given their quantum origin, it is natural to wonder whether sampling a DPP on a classical computer is easier than on a classical one. Vanilla sampling consists in two steps, of respective costs $mathcalO(N3)$ and $mathcalO(Nr2)$ operations on a classical computer, where $r$ is the rank of the kernel matrix.
  arXiv  Detail & Related papers  (2023-05-25T08:43:11Z)
• The Sample Complexity of One-Hidden-Layer Neural Networks [57.6421258363243]
  We study a class of scalar-valued one-hidden-layer networks, and inputs bounded in Euclidean norm. We prove that controlling the spectral norm of the hidden layer weight matrix is insufficient to get uniform convergence guarantees. We analyze two important settings where a mere spectral norm control turns out to be sufficient.
  arXiv  Detail & Related papers  (2022-02-13T07:12:02Z)

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.