pith. sign in

arxiv: 2604.20793 · v2 · submitted 2026-04-22 · 💻 cs.CR

Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

Ray Iskander , Khaled Kirah This is my paper

Pith reviewed 2026-05-10 00:18 UTC · model grok-4.3

classification 💻 cs.CR
keywords NTTarithmetic maskingpipeline compositionpost-quantum cryptographyhardware securitymachine-checked proofsside-channel resistancebutterfly operation
0
0 comments X

The pith

Fresh independent masks at each NTT butterfly stage produce uniform output distributions independent of secrets at every pipeline position.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that supplying a new random mask for the output of every butterfly stage in a Number Theoretic Transform pipeline makes every intermediate wire carry a uniform distribution that reveals nothing about the secret inputs under first-order probing. It proves this for the basic butterfly over any modulus and then lifts the result to an arbitrary number of pipeline stages. A reader would care because post-quantum hardware accelerators need fast pipelined arithmetic that still resists side-channel attacks without adding large overhead or extra randomness sources. The proofs are written as machine-checked statements that hold for any twiddle factor and any input value. They also explain why some existing accelerators leak: they apply masking only at the start rather than refreshing it at each stage.

Core claim

For any Cooley-Tukey butterfly with a fresh output mask over the integers modulo q, each output wire takes every possible value exactly once as the mask varies, producing a uniform marginal distribution independent of the secret inputs and the twiddle factor; this property lifts to any k-stage pipeline when each stage receives its own independent fresh mask, satisfying per-context uniformity at every stage under the first-order probing model.

What carries the argument

Per-context uniformity of a masked arithmetic butterfly, the property that each output wire receives every value exactly once for each fixed input context when the output mask is chosen uniformly at random.

If this is right

  • Any number of NTT stages can be placed in series while preserving first-order security provided each stage receives its own fresh mask.
  • The uniformity result holds for every modulus q, every twiddle factor, and every input value.
  • Pointwise value-independence between secret and masked values does not hold for butterfly outputs, yet the marginal distribution remains uniform under fresh masking.
  • Accelerators that mask only the initial input and reuse the same mask through later stages violate the composition requirement and lose the uniformity guarantee.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Hardware designs must include dedicated random-bit generators sized to supply a new mask for every butterfly in every cycle.
  • The same fresh-mask discipline is likely required for other nonlinear operations such as modular reduction if full pipeline security is desired.
  • The machine-checked statements provide a template that can be reused to verify higher-order probing resistance once the corresponding masking gadgets are formalized.
  • Architectural reviews of existing PQC accelerators can now check mask-renewal points as a first-pass security audit.

Load-bearing premise

Independent fresh randomness must be supplied for the output mask of every butterfly stage.

What would settle it

A concrete two-stage NTT pipeline supplied with fresh per-stage masks in which the distribution of an output wire at the second stage depends on the secret input value.

read the original 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 $\mathbb{Z}_q$. 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 $\mathrm{GF}(2)$; no proof assistant artifact addresses the NTT butterfly over $\mathbb{Z}_q$. 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, butterfly per-context uniformity: for any Cooley-Tukey butterfly with fresh output mask over $\mathbb{Z}/q\mathbb{Z}$ ($q > 0$), each output wire has exactly one mask value producing each output, a uniform marginal independent of secrets, universal over all moduli, twiddle factors, and inputs. Third, a k-stage NTT pipeline with fresh per-stage masking satisfies per-context uniformity at every stage under the ISW first-order probing model. We document a named warning: pointwise value-independence is false for butterfly outputs. The Adams Bridge accelerator (CHIPS Alliance Caliptra) fails the fresh masking hypothesis, masking active only in INTT round 0, architecturally explaining its structural insecurity. Artifact: nine theorems, 1,738 build jobs, zero sorry. Composition for nonlinear gadgets (Barrett) is addressed in forthcoming manuscripts proving Barrett's PF-PINI(2) satisfaction (one-bit barrier) [3] and k-stage composition for PF-PINI gadgets under fresh-mask renewal [4].

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper claims that a k-stage NTT pipeline over Z/qZ with fresh per-stage arithmetic masking satisfies per-context uniformity at every stage under the ISW first-order probing model. This is established by three machine-checked Lean 4 theorems (zero sorries) against Mathlib: (1) value-independence implies constant marginal distributions via an algebraic MutualInfoZero proxy, (2) per-context uniformity for any Cooley-Tukey butterfly with fresh output masks (universal over all moduli, twiddles, and inputs), and (3) inductive composition to k stages. The fresh-masking hypothesis is explicitly required; a counterexample (Adams Bridge accelerator) is given when it is violated. The work closes a gap in prior composition frameworks, which were limited to Boolean masking.

Significance. If the results hold, the contribution is significant for formal security analysis of PQC hardware. It supplies the first machine-checked proofs for arithmetic masking in NTT butterflies, extending ISW-style composition from GF(2) to Z/qZ with universal, parameter-free statements. The explicit fresh-masking requirement, named warning on pointwise value-independence, and architectural explanation of the Adams Bridge insecurity provide actionable guidance for ML-KEM/ML-DSA accelerators. The artifact (nine theorems, 1738 build jobs, zero sorries) sets a high standard for reproducibility in the field.

minor comments (2)
  1. Abstract states 'nine theorems' but describes three main results; a short table or paragraph in §1 or §4 clarifying the full theorem count and their dependencies would improve readability.
  2. The manuscript notes that nonlinear-gadget composition (e.g., Barrett) is deferred to forthcoming work; a brief forward reference in the conclusion to the PF-PINI results would help readers assess the current scope.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful reading and for recommending acceptance. The provided summary accurately captures the scope and results of the manuscript.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's central claims are three machine-checked Lean 4 theorems (zero sorries) that derive value-independence implying constant marginals, butterfly per-context uniformity for fresh output masks over Z/qZ, and k-stage NTT pipeline composability directly from the formal definitions of the Cooley-Tukey butterfly and the ISW first-order probing model. These universal statements hold for arbitrary moduli, twiddle factors, and inputs under the explicitly required fresh-masking hypothesis, with an explicit counterexample (Adams Bridge) when the hypothesis is violated. Prior self-citations supply context on structural analysis but are not load-bearing; the new results are self-contained formal verifications with no reduction to fitted parameters, self-referential quantities, or unverified ansatzes.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The proofs rest on standard formalizations of modular arithmetic and the ISW probing model already present in Mathlib; no new entities, fitted constants, or ad-hoc axioms are introduced by the paper.

axioms (2)
  • standard math Standard properties of Z/qZ and Cooley-Tukey butterflies as encoded in Mathlib
    Invoked to define the butterfly operation and prove uniformity for arbitrary q, twiddles, and inputs.
  • domain assumption Semantics of the ISW first-order probing model
    Used to interpret per-context uniformity as security against first-order probes.

pith-pipeline@v0.9.0 · 5676 in / 1395 out tokens · 54469 ms · 2026-05-10T00:18:23.623322+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

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

    cs.CR 2026-04 accept novelty 8.0 partial

    Machine-checked Lean proofs show that fresh inter-stage masking in prime-field PINI gadgets erases prior multiplicity, satisfying only the second gadget's security parameter.

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

    cs.CR 2026-04 unverdicted novelty 8.0

    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 Ada...

  3. The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

    cs.CR 2026-05 conditional novelty 7.0 full

    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.

  4. Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

    cs.CR 2026-04 unverdicted novelty 6.0 partial

    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.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages · cited by 3 Pith papers · 3 internal anchors

  1. [1]

    Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators

    R. Iskander and K. Kirah, “Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators,” arXiv:2604.15249, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  2. [2]

    Partial Number Theoretic Transform Masking in Post-Quantum Cryptography (PQC) Hardware: A Security Margin Analysis

    R. Iskander and K. Kirah, “Partial NTT Masking in Post-Quantum Cryptography Hardware: A Security Margin Analysis,” arXiv:2604.03813, 2026. 15

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  3. [3]

    The 1-Bit Barrier: A Machine-Checked Trichotomy for Barrett Reduction in Masked PQC Hardware

    R. Iskander and K. Kirah, “The 1-Bit Barrier: A Machine-Checked Trichotomy for Barrett Reduction in Masked PQC Hardware”, Manuscript under preparation

    work page

  4. [4]

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

    R. Iskander and K. Kirah, “Prime-Field PINI: Machine-Checked Composition Theorems for Post- Quantum NTT Masking”, Manuscript under preparation

    work page

  5. [5]

    Module-Lattice-Based Key-Encapsulation Mechanism Standard (FIPS 203),

    NIST, “Module-Lattice-Based Key-Encapsulation Mechanism Standard (FIPS 203),” 2024

    work page 2024

  6. [6]

    Private Circuits: Securing Hardware against Probing Attacks,

    Y. Ishai, A. Sahai, and D. Wagner, “Private Circuits: Securing Hardware against Probing Attacks,” CRYPTO 2003, LNCS 2729, pp. 463-481

    work page 2003

  7. [7]

    Strong Non-Interference and Type-Directed Higher-Order Masking,

    G. Barthe, S. Belaid, F. Dupressoir, P.-A. Fouque, B. Gregoire, P.-Y. Strub, and R. Zucchini, “Strong Non-Interference and Type-Directed Higher-Order Masking,” CCS 2016, pp. 116-129

    work page 2016

  8. [8]

    Trivially and Efficiently Composing Masked Gadgets with Probe Isolating Non-Interference,

    G. Cassiers and F.-X. Standaert, “Trivially and Efficiently Composing Masked Gadgets with Probe Isolating Non-Interference,” IEEE TIFS, vol. 15, pp. 2542-2555, 2020. (CHES 2020)

    work page 2020

  9. [9]

    Domain-Oriented Masking: Compact Masked Hardware Implementations with Arbitrary Protection Order,

    H. Gross, S. Mangard, and T. Korak, “Domain-Oriented Masking: Compact Masked Hardware Implementations with Arbitrary Protection Order,” TIS@CCS 2016

    work page 2016

  10. [10]

    Verified Proofs of Higher-Order Masking,

    G. Barthe, S. Belaid, F. Dupressoir, P.-A. Fouque, B. Gregoire, and P.-Y. Strub, “Verified Proofs of Higher-Order Masking,” EUROCRYPT 2015, LNCS 9056, pp. 457-485

    work page 2015

  11. [11]

    SILVER – Statistical Independence and Leakage Verification,

    D. Knichel, P. Sasdrich, and A. Moradi, “SILVER – Statistical Independence and Leakage Verification,” ASIACRYPT 2020, LNCS 12491, pp. 787-816

    work page 2020

  12. [12]

    Coco-Alma: A Versatile Masking Verifier,

    V. Hadzic and R. Bloem, “Coco-Alma: A Versatile Masking Verifier,” FMCAD 2021

    work page 2021

  13. [13]

    The Lean 4 Theorem Prover and Programming Language,

    L. de Moura and S. Ullrich, “The Lean 4 Theorem Prover and Programming Language,” CADE 2021, LNCS 12699, pp. 625-635

    work page 2021

  14. [14]

    Mathlib4: The Lean 4 Mathematical Library,

    The mathlib Community, “Mathlib4: The Lean 4 Mathematical Library,” https://github.com/leanprover-community/mathlib4

    work page

  15. [15]

    From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

    R. Iskander and K. Kirah, “From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification,”, arXiv:2604.18717, 2026. https://github.com/rayiskander2406/qanary-universal-masking-proofs-arXiv-2604.18717

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  16. [16]

    Security Requirements for Cryptographic Modules (FIPS 140-3),

    NIST, “Security Requirements for Cryptographic Modules (FIPS 140-3),” 2019

    work page 2019

  17. [17]

    Adams Bridge: Post-Quantum Cryptographic Accelerator,

    CHIPS Alliance, “Adams Bridge: Post-Quantum Cryptographic Accelerator,” https://github.com/chipsalliance/adams-bridge

    work page

  18. [18]

    Module-Lattice-Based Digital Signature Standard (FIPS 204),

    NIST, “Module-Lattice-Based Digital Signature Standard (FIPS 204),” 2024

    work page 2024

  19. [19]

    Composable Masking Schemes in the Presence of Physical Defaults and the Robust Probing Model,

    S. Faust, V. Grosso, S. Merino Del Pozo, C. Paglialonga, and F.-X. Standaert, “Composable Masking Schemes in the Presence of Physical Defaults and the Robust Probing Model,” TCHES 2018(3), pp. 89-120

    work page 2018

  20. [20]

    Formal Verification of Masked Hardware Implementations in the Presence of Glitches,

    R. Bloem, H. Gross, R. Iusupov, B. Konighofer, S. Mangard, and J. Winter, “Formal Verification of Masked Hardware Implementations in the Presence of Glitches,” EUROCRYPT 2018, LNCS 10821, pp. 321-353

    work page 2018

  21. [21]

    Formal Verification of Arithmetic Masking in Hardware and Software,

    B. Gigerl, R. Primas, and S. Mangard, “Formal Verification of Arithmetic Masking in Hardware and Software,” ACNS 2023, LNCS 13905

    work page 2023

  22. [22]

    Conversion from Arithmetic to Boolean Masking with Logarithmic Complexity,

    J.-S. Coron, J. Grossschadl, M. Tibouchi, and P. K. Vadnala, “Conversion from Arithmetic to Boolean Masking with Logarithmic Complexity,” FSE 2015, LNCS 9054, pp. 130-149. 16

    work page 2015

  23. [23]

    PFR: Polynomial Freiman-Ruzsa Conjecture – Lean 4 Formalization,

    T. Tao et al., “PFR: Polynomial Freiman-Ruzsa Conjecture – Lean 4 Formalization,” https://github.com/teorth/pfr

    work page

  24. [24]

    Transition to Post-Quantum Cryptography Standards (IR 8547),

    NIST, “Transition to Post-Quantum Cryptography Standards (IR 8547),” 2025

    work page 2025