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

Computer Science > Cryptography and Security [Submitted on 28 Apr 2026] Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking Ray Iskander, Khaled Kirah 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. Comments: 17 pages, 1 Figure Subjects: Cryptography and Security (cs.CR) Cite as: arXiv:2604.25878 [cs.CR]   (or arXiv:2604.25878v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2604.25878 Focus to learn more Submission history From: Khaled Kirah Dr [view email] [v1] Tue, 28 Apr 2026 17:21:20 UTC (479 KB) Access Paper: view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-04 Change to browse by: cs References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)