Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking
2026-04-28 • Cryptography and Security
Cryptography and Security
AI summaryⓘ
The authors study how to securely combine arithmetic masking techniques in hardware for post-quantum cryptography, focusing on operations over prime fields like those used in NTT (Number Theoretic Transform). They prove new theorems showing that inserting fresh random masks between stages makes intermediate data perfectly secure, removing vulnerabilities. Their formal proofs, done in the Lean 4 system, also reveal a security flaw in Microsoft’s Adams Bridge accelerator where missing fresh masking leaves the chip open to attacks. This work bridges theory and real hardware and confirms earlier empirical findings about these vulnerabilities.
arithmetic maskingprime fieldspost-quantum cryptographyNumber Theoretic Transform (NTT)Probing modelBarrett reductiondifferential power analysisformal verificationLean 4hardware security
Authors
Ray Iskander, Khaled Kirah
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.