Machine-checked Lean 4 proofs establish PF-PINI composition theorems for prime-field arithmetic masking, showing fresh inter-stage masks erase prior security parameters and diagnosing non-uniformity in Microsoft's Adams Bridge PQC accelerator.
Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
abstract
Post-quantum cryptographic (PQC) accelerators implementing ML-KEM (FIPS 203) and ML-DSA (FIPS 204) require side-channel resistance evidence for FIPS 140-3 certification. However, exact masking-verification tools scale only to gadgets of a few thousand cells. We present a four-stage verification hierarchy, D0/D1 structural dependency analysis, fresh-mask refinement, Boolean Single-Authentication Distance Checking (SADC), and arithmetic SADC, that extends sound first-order masking verification to production arithmetic modules. Applied to the 1.17-million-cell Adams Bridge ML-DSA/ML-KEM accelerator, structural analysis completes in seconds across all 30 masked submodules. A multi-cycle extension (MC-D1) reclassifies 12 modules from structurally clean to structurally flagged. On the 5,543-cell ML-KEM Barrett reduction module, the pipeline machine-verifies 198 of 363 structurally flagged wires (54.5%) as first-order secure, reports 165 as candidate insecure for designer triage (a sound upper bound), and leaves 0 indeterminate. Every verdict is cross validated by Z3 and CVC5 with 0 disagreements across 363 wires. The result narrows manual review from hundreds of structural flags to 165 actionable candidates with mathematical certificates, enabling pre-silicon side-channel evidence generation on production ML-KEM hardware.
citation-role summary
background 1
citation-polarity summary
fields
cs.CR 6years
2026 6roles
background 1polarities
background 1representative citing papers
Machine-checked proofs establish that fresh per-stage masking in Cooley-Tukey NTT pipelines over Z/qZ yields per-context uniformity at every stage under the ISW first-order probing model.
A Lean 4 formalization proves that value-independence implies identical marginal distributions for masking verification across all positive integers q.
Strategic masking of three consecutive mid-layers in NTT hardware defeats soft-analytical side-channel attacks with only 43% overhead while single-layer masking plus shuffling falls short of claimed 2^46–2^96 margins.
Arbitrary-depth k-stage masked NTT pipelines with fresh inter-stage masking and PF-PINI(≤2) gadgets satisfy a universal 2/q per-observation leakage bound, machine-checked in Lean 4.
Barrett reduction's masked internal map has preimage sizes in {0,1,2}, establishing a universal 1-bit leakage barrier, with the trichotomy and PF-PINI properties machine-checked in Lean 4.
citing papers explorer
-
Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking
Machine-checked Lean 4 proofs establish PF-PINI composition theorems for prime-field arithmetic masking, showing fresh inter-stage masks erase prior security parameters and diagnosing non-uniformity in Microsoft's Adams Bridge PQC accelerator.
-
Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware
Machine-checked proofs establish that fresh per-stage masking in Cooley-Tukey NTT pipelines over Z/qZ yields per-context uniformity at every stage under the ISW first-order probing model.
-
From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification
A Lean 4 formalization proves that value-independence implies identical marginal distributions for masking verification across all positive integers q.
-
Partial Number Theoretic Transform Masking in Post-Quantum Cryptography (PQC) Hardware: A Security Margin Analysis
Strategic masking of three consecutive mid-layers in NTT hardware defeats soft-analytical side-channel attacks with only 43% overhead while single-layer masking plus shuffling falls short of claimed 2^46–2^96 margins.
-
The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware
Arbitrary-depth k-stage masked NTT pipelines with fresh inter-stage masking and PF-PINI(≤2) gadgets satisfy a universal 2/q per-observation leakage bound, machine-checked in Lean 4.
-
Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware
Barrett reduction's masked internal map has preimage sizes in {0,1,2}, establishing a universal 1-bit leakage barrier, with the trichotomy and PF-PINI properties machine-checked in Lean 4.