The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware
Ray Iskander, Khaled Kirah
cs.CR
May 4, 2026 · v1
TL;DR
Machine-checks in Lean 4 cardinality and leakage bounds for masked NTT pipelines in post-quantum cryptography hardware.
Abstract
This is Paper 7 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. 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 q^{2k-2}$ on the preimage of any output value, machine-checked in Lean 4 with zero \texttt{sorry}. Under the standard (informal) semantic translation that divides this cardinality by the total mask-tuple space size $q^{2k-1}$, the per-observation conditional probability bound is $2/q$, independent of pipeline depth $k$. The QANARY program has previously established machine-checked cardinality bounds on the per-observation leakage of masked NTT hardware: PF-PINI(2) for Barrett reduction (Paper 5 [3]), 2-stage composition with fresh inter-stage masking (Paper 6 [4]), an underlying universality theorem (Paper 3 [5]), and PF-PINI(1) for butterfly wires (Paper 4 [6]). This paper closes the program with four contributions. First, a $k$-stage composition theorem generalizing Paper 6's two-stage result to arbitrary $k \geq 1$ gives the last-stage-determined bound $G_{k-1}.\texttt{maxMult} \cdot q^{2k-2}$: only the last stage's PF-PINI parameter survives, with intermediate parameters erased by fresh inter-stage masking. Second, Montgomery reduction satisfies PF-PINI(2) with tight max-multiplicity 2. Third, we assemble these into the end-to-end bound $2 \cdot q^{2k-2}$ for any depth-$k$ PF-PINI($\leq 2$) pipeline under fresh inter-stage masking. Fourth, a Lean-verified hypothesis-violation conditional anchors the prior empirical and structural Adams Bridge analyses ([1, 2, 7, 8]).
Problem
Masked NTT pipelines for post-quantum cryptography hardware require formal security guarantees that leakage bounds hold regardless of pipeline depth, but prior work only covered two-stage composition and specific gadgets like Barrett reduction.
Approach
The paper proves a k-stage composition theorem generalizing prior two-stage results to arbitrary depth k >= 1, showing that only the last stage's PF-PINI parameter survives when fresh inter-stage masking is applied. It also establishes PF-PINI(2) with tight max-multiplicity 2 for Montgomery reduction. These are assembled into an end-to-end bound of 2*q^(2k-2) for any depth-k PF-PINI(<=2) pipeline. All results are machine-checked in Lean 4 with zero sorry axioms.
Results
The per-observation conditional probability bound is 2/q, independent of pipeline depth k. This closes the QANARY formal verification program by covering all standard modular reductions (Barrett and Montgomery) and arbitrary pipeline depths with machine-checked proofs.
