The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware
2026-05-04 • Cryptography and Security
Cryptography and Security
AI summaryⓘ
The authors continue their formal study of masked Number Theoretic Transform (NTT) hardware used in post-quantum cryptography, extending previous work that analyzed security bounds for two-stage pipelines to arbitrary-length pipelines. They prove that only the last stage's masking parameter affects the security bound, while earlier stages' parameters are effectively hidden by fresh inter-stage masking. The paper also shows that Montgomery reduction, a key arithmetic step, satisfies the required security property with a tight bound. All these results are machine-checked in Lean 4, providing strong formal assurance of the security limits for masked NTT pipelines.
Number Theoretic Transform (NTT)Masked hardwarePost-quantum cryptographyFormal verificationLean 4PF-PINI gadgetsMontgomery reductionCardinality boundFresh inter-stage maskingPipeline composition
Authors
Ray Iskander, Khaled Kirah
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]).