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

TL;DR

This paper presents the first machine-checked theorems for arithmetic masking over prime fields in post-quantum cryptography, formalizing security properties and diagnosing vulnerabilities in hardware implementations.

Contribution

It introduces novel formal composition theorems for prime-field masking, bridging algebraic and hardware models, and applies them to analyze a real cryptographic accelerator.

Findings

Formalized theorems in Lean 4 with 18 proofs and no stubs.

Diagnosed a security flaw in Microsoft's PQC accelerator due to lack of fresh masking.

Suggests the 1-Bit Barrier is universal across Barrett and Montgomery reductions.

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.