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.
Partial Number Theoretic Transform Masking in Post-Quantum Cryptography (PQC) Hardware: A Security Margin Analysis
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
abstract
Adams Bridge, a hardware accelerator for ML-DSA and ML-KEM designed for the Caliptra root of trust, masks 1 of its Inverse Number Theoretic Transform (INTT) layers and relies on shuffling for the remainder, claiming per-butterfly Correlation Power Analysis (CPA) complexities of 2^46 (ML-DSA) and 2^96 (ML-KEM). We evaluate these claims against published side-channel literature across seven analysis tracks with confidence-rated evidence. Register-Transfer Level (RTL) analysis confirms that the design's Random Start Index (RSI) shuffling provides 6 bits of entropy per layer (64 orderings) rather than the 296 bits of a full random permutation assumed in its scaling argument, with effective margins below the designers' estimates. A soft-analytical attack pipeline demonstrates a 37-bit enumeration reduction, independent of Belief Propagation (BP) gains, quantifying the attack-model gap without achieving key recovery. Full-scale BP on the complete INTT factor graph achieves 100% coefficient recovery over the single-layer baseline, resolving whether BP gains scale to production-size Number Theoretic Transform (NTT) structures. A genie-aided information-theoretic bound shows observations contain sufficient mutual information for full recovery at SNRxN as low as 15. Layer-ablation analysis identifies four necessary conditions governing BP convergence. Observation topology, not count, determines recovery: 4 evenly spread layers achieve 100% while 4 consecutive layers achieve 0%, yielding a practical countermeasure design tool. Strategic masking of 3 consecutive mid-layers (43% overhead vs. full masking) creates an unrecoverable gap that defeats soft-analytical attacks. We contribute a reusable security margin audit methodology combining RTL verification, epistemic confidence tagging, sensitivity-scenario analysis, and experimental validation applicable to any partially masked NTT accelerator.
fields
cs.CR 6years
2026 6representative 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.
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.
A four-stage hierarchy (D0/D1 structural analysis, mask refinement, Boolean and arithmetic SADC) machine-verifies 198 of 363 flagged wires as first-order secure on a 5543-cell ML-KEM module with zero indeterminates and cross-solver agreement.
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.
-
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.
-
Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators
A four-stage hierarchy (D0/D1 structural analysis, mask refinement, Boolean and arithmetic SADC) machine-verifies 198 of 363 flagged wires as first-order secure on a 5543-cell ML-KEM module with zero indeterminates and cross-solver agreement.
-
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.