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

From bibtex.

Abstract

Boolean masking composition is well-understood through NI, SNI, and PINI. Arithmetic masking over 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 k1 and k2, the composed two-stage pipeline with fresh masking satisfies PF-PINI(k2); Stage 1's multiplicity is completely erased from the composed output. Without fresh masking, intermediate wires have multiplicity up to k1, 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.