Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware
Ray Iskander, Khaled Kirah

TL;DR
This paper proves machine-checked security properties of arithmetic masking in NTT pipelines for PQC hardware, demonstrating that fresh per-stage masking guarantees security at the pipeline level with formal proofs in Lean 4.
Contribution
It provides the first formal, machine-checked proofs that per-stage fresh masking ensures pipeline-level security in NTT-based PQC accelerators.
Findings
Per-stage masking guarantees uniformity and security in NTT pipelines.
Butterfly outputs are not pointwise value-independent, revealing security limitations.
The Adams Bridge accelerator's architecture explains its structural insecurity.
Abstract
Post-quantum cryptographic (PQC) accelerators for ML-KEM (FIPS 203) and ML-DSA (FIPS 204) rely on pipelined Number Theoretic Transform (NTT) stages over . Our prior work established structural dependency analysis at scale [1] and quantified the security margin of partial NTT masking [2]. Whether per-stage arithmetic masking guarantees pipeline-level security had no prior machine-checked answer for the r-bearing case: composition frameworks (ISW, t-SNI, PINI, DOM) were formalized exclusively for Boolean masking over ; no proof assistant artifact addresses the NTT butterfly over . We present three machine-checked results in Lean 4 with Mathlib, all zero sorry. First, we close a stated limitation of prior work: value-independence implies constant marginal distribution under fresh randomness (via an algebraic MutualInfoZero proxy). Second,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
