pith. sign in

arxiv: 2605.02856 · v2 · submitted 2026-05-04 · 💻 cs.CR

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

Ray Iskander , Khaled Kirah This is my paper

Pith reviewed 2026-05-08 18:04 UTC · model grok-4.3

classification 💻 cs.CR
keywords post-quantum cryptographymasked implementationsnumber-theoretic transformpipeline compositionleakage boundsmodular reductionside-channel analysis
0
0 comments X

The pith

Masked number-theoretic transform pipelines of any depth maintain a leakage probability bound of 2/q under fresh inter-stage masking.

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

The paper establishes that masked pipelines for the number-theoretic transform in post-quantum cryptography hardware can have any number of stages without increasing the per-observation leakage probability beyond 2/q. This holds when fresh masks are inserted between stages and each modular reduction gadget meets a basic per-stage security property. The result unifies bounds across different reductions and extends the analysis from two stages to arbitrary depth. If correct, hardware designers gain flexibility to pipeline for higher throughput while preserving the same side-channel security level. The central argument relies on counting the size of the preimage sets for output values under the masking scheme.

Core claim

Arbitrary-depth k-stage masked pipelines for the number-theoretic transform with fresh inter-stage masking and per-stage gadgets satisfying the required security property with parameter at most 2 satisfy a per-observation cardinality bound of 2 times q to the power of 2k minus 2 on the preimage of any output value. Under the division by the mask-tuple space size q to the power of 2k minus 1, this yields a conditional probability bound of 2/q that does not depend on the pipeline depth k. The analysis covers standard modular reductions and shows the bound is determined solely by the final stage.

What carries the argument

k-stage composition under fresh inter-stage masking, which erases the security parameters of all intermediate stages leaving only the last stage's parameter in the overall bound.

If this is right

  • The leakage probability remains capped at 2/q for pipelines of any length k.
  • Both Barrett and Montgomery reductions fit under the same unified bound when they satisfy the per-stage property.
  • The overall security depends only on the final stage after fresh masking is applied between stages.
  • The base case for one stage reduces to the gadget property itself.

Where Pith is reading between the lines

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

  • Designers may increase pipeline depth to improve clock frequency or throughput without needing to strengthen masking in earlier stages.
  • The composition rule could apply to other multi-stage arithmetic circuits in cryptography if they use similar masking.
  • Verification work can focus on proving the property for individual gadgets rather than the full pipeline.
  • Accepting the probability translation would allow direct use of the bound in security evaluations of pipelined accelerators.

Load-bearing premise

The informal mapping from the preimage cardinality to the conditional probability bound holds, along with the assumption that each per-stage gadget satisfies the necessary security property.

What would settle it

A concrete example for some k greater than 2 where the number of input mask combinations mapping to one output exceeds 2 times q to the power of 2k minus 2, or an implementation where observed leakage probability surpasses 2/q.

read the original abstract

This is Paper 7 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. Arbitrary-depth $k$-stage masked NTT pipelines with fresh inter-stage masking and per-stage PF-PINI($\leq 2$) gadgets satisfy a per-observation cardinality bound of $2 \cdot q^{2k-2}$ on the preimage of any output value, machine-checked in Lean 4 with zero \texttt{sorry}. Under the standard (informal) semantic translation that divides this cardinality by the total mask-tuple space size $q^{2k-1}$, the per-observation conditional probability bound is $2/q$, independent of pipeline depth $k$. The QANARY program has previously established machine-checked cardinality bounds on the per-observation leakage of masked NTT hardware: PF-PINI(2) for Barrett reduction (Paper 5 [3]), 2-stage composition with fresh inter-stage masking (Paper 6 [4]), an underlying universality theorem (Paper 3 [5]), and PF-PINI(1) for butterfly wires (Paper 4 [6]). This paper closes the program with four contributions. First, a $k$-stage composition theorem generalizing Paper 6's two-stage result to arbitrary $k \geq 1$ gives the last-stage-determined bound $G_{k-1}.\texttt{maxMult} \cdot q^{2k-2}$: only the last stage's PF-PINI parameter survives, with intermediate parameters erased by fresh inter-stage masking. Second, Montgomery reduction satisfies PF-PINI(2) with tight max-multiplicity 2. Third, we assemble these into the end-to-end bound $2 \cdot q^{2k-2}$ for any depth-$k$ PF-PINI($\leq 2$) pipeline under fresh inter-stage masking. Fourth, a Lean-verified hypothesis-violation conditional anchors the prior empirical and structural Adams Bridge analyses ([1, 2, 7, 8]).

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

1 major / 1 minor

Summary. The manuscript (Paper 7 in the QANARY series) proves a k-stage composition theorem for masked NTT pipelines in PQC hardware. With fresh inter-stage masking and per-stage PF-PINI(≤2) gadgets, any output value has at most 2 · q^{2k-2} preimages under the composition; this cardinality bound is machine-checked in Lean 4 with zero sorry statements. The paper also establishes PF-PINI(2) for Montgomery reduction (with maxMult=2) and assembles these into an end-to-end cardinality bound. Under the standard informal semantic translation that divides the cardinality by the mask-tuple space size q^{2k-1}, the per-observation conditional probability is bounded by 2/q independently of pipeline depth k. A Lean-verified hypothesis-violation conditional for prior Adams Bridge analyses is included.

Significance. If the informal translation holds, the result establishes a universal 1-bit leakage barrier for arbitrary-depth masked NTT pipelines, independent of k. The zero-sorry Lean 4 machine-checked proofs for the cardinality bound and composition theorem constitute a major strength, supplying high-assurance formal support that closes the series. This advances the application of interactive theorem proving to side-channel security analysis of post-quantum cryptography hardware.

major comments (1)
  1. [Abstract] Abstract and main theorem statement: the per-observation conditional probability bound of 2/q is obtained solely by dividing the machine-checked cardinality 2 · q^{2k-2} by q^{2k-1}. This step assumes uniform independent sampling of the 2k-1 mask tuples, that the observation is a deterministic function of the masks (or masks plus secret, independent of the secret), and that no additional leakage channels arise. The text labels the step “standard (informal)” but provides no formal statement of the observation predicate or proof that the division yields the claimed conditional probability under the concrete hardware leakage model; this translation is load-bearing for the probability claim that underpins the “1-bit barrier is universal” title.
minor comments (1)
  1. [Introduction] The PF-PINI(≤2) assumption for all per-stage gadgets (including the newly proved Montgomery case) is referenced to prior papers in the series; a short self-contained recap of the exact PF-PINI definition and the maxMult parameter would improve readability for readers who have not followed the entire series.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation of the machine-checked proofs and for the constructive comment. We address the major comment below and accept it as a point for minor revision to improve clarity.

read point-by-point responses

  1. Referee: [Abstract] Abstract and main theorem statement: the per-observation conditional probability bound of 2/q is obtained solely by dividing the machine-checked cardinality 2 · q^{2k-2} by q^{2k-1}. This step assumes uniform independent sampling of the 2k-1 mask tuples, that the observation is a deterministic function of the masks (or masks plus secret, independent of the secret), and that no additional leakage channels arise. The text labels the step “standard (informal)” but provides no formal statement of the observation predicate or proof that the division yields the claimed conditional probability under the concrete hardware leakage model; this translation is load-bearing for the probability claim that underpins the “1-bit barrier is universal” title.

    Authors: We agree that the 2/q probability bound follows from dividing the machine-checked cardinality 2 · q^{2k-2} by the mask space size q^{2k-1} and that this step is informal, as the manuscript already states. The primary formal result is the cardinality bound, which has been verified in Lean 4 with zero sorry statements and holds for arbitrary pipeline depth k under fresh inter-stage masking and per-stage PF-PINI(≤2) gadgets. This generalizes the two-stage composition from Paper 6, with only the final stage's maxMult parameter surviving due to the fresh masking between stages. The assumptions of uniform independent sampling of the 2k-1 masks, deterministic observation as a function of the masks (and secret), and no extraneous leakage channels are the standard modeling choices in the masking literature and have been used consistently across the QANARY series. We do not supply a formal observation predicate or a proof of the conditional probability under a specific hardware leakage model (e.g., power or EM) because the paper's scope is the combinatorial preimage analysis, which supplies a worst-case bound independent of the precise leakage function. To address the referee's concern about the load-bearing nature of the translation for the title claim, we will revise the abstract and the main theorem statement to explicitly enumerate these three assumptions. This makes the informal step more transparent without altering any formal results or proofs. revision: yes

Circularity Check

0 steps flagged

No significant circularity; central claims grounded in independent Lean formalization

full rationale

The paper derives the k-stage cardinality bound 2·q^{2k-2} and the resulting 2/q probability claim through a new composition theorem that generalizes the two-stage result from prior work, together with a fresh proof that Montgomery reduction satisfies PF-PINI(≤2). Both the composition and the Montgomery property are machine-checked in Lean 4 with zero 'sorry' statements, making the derivation self-contained against an external formal-verification benchmark rather than reducing to any fitted parameter, self-referential definition, or unverified self-citation. The cited papers in the series supply the PF-PINI assumptions for other gadgets, but these are treated as independently established inputs; the new theorem erases intermediate parameters via fresh masking and does not rely on any load-bearing self-citation chain. The informal division of cardinality by mask-space size q^{2k-1} is a standard semantic modeling step, not a circular reduction of the result to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the PF-PINI(≤2) security properties of the per-stage gadgets (including the newly verified Montgomery case) and the assumption of fresh independent inter-stage masking; these are treated as domain assumptions carried forward from the series rather than re-derived here.

axioms (2)
  • domain assumption Every per-stage gadget satisfies PF-PINI with parameter at most 2.
    Invoked in the composition theorem; established for Barrett in prior work and proven here for Montgomery.
  • domain assumption Fresh, independent random masks are applied between every pair of stages.
    Required for the erasure of intermediate PF-PINI parameters in the k-stage bound.

pith-pipeline@v0.9.0 · 5719 in / 1635 out tokens · 66839 ms · 2026-05-08T18:04:08.601588+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages · 6 internal anchors

  1. [1]

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

    Iskander, Kirah, Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators, arXiv:2604.15249 (Paper 1 of QANARY program). https://arxiv.org/abs/2604.15249. (Verification chain: arXiv listing v2 2026-04-20; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-16, v2 ...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.5281/zenodo.19625392 2026

  2. [2]

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

    Iskander, Kirah, Partial Number Theoretic Transform Masking in Post-Quantum Cryptography (PQC) Hardware: A Security Margin Analysis, arXiv:2604.03813 (Paper 2 of QANARY program). https://arxiv.org/abs/2604.03813. (Verification chain: arXiv listing v2 2026-04-17; primary subject cs.CR; authors Iskander, Kirah; v1 28 submitted 2026-04-04, v2 replaced 2026-0...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.5281/zenodo.19508454 2026

  3. [3]

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

    Iskander, Kirah, Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware, arXiv:2604.24670 (Paper 5 of QANARY program). https://arxiv.org/abs/2604.24670. (Verification chain: arXiv listing 2026-04-27; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-27...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.5281/zenodo.19842166 2026

  4. [4]

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

    Iskander, Kirah, Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking, arXiv:2604.25878 (Paper 6 of QANARY program). https://arxiv.org/abs/2604.25878. (Verification chain: arXiv listing v1 2026-04-28; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-28 (publicly listed 2026-04-29). Zenodo concept DOI: 10....

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.5281/zenodo.19905303 2026

  5. [5]

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

    Iskander, Kirah, From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification, arXiv:2604.18717 (Paper 3 of QANARY program). https://arxiv.org/abs/2604.18717. (Verification chain: arXiv listing 2026-04-22; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-20, v2 replaced 2026-04-22. Zenodo...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.5281/zenodo.19689480 2026

  6. [6]

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

    Iskander, Kirah, Fresh Masking Makes NTT Pipelines Composable: Machine- Checked Proofs for Arithmetic Masking in PQC Hardware, arXiv:2604.20793 (Paper 4 of QANARY program). https://arxiv.org/abs/2604.20793. (Verification chain: arXiv listing v2 2026-04-25; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-22 (publicly listed 2026-04-23)...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.5281/zenodo.19705450 2026

  7. [7]

    Karabulut, M., Azarderakhsh, R., Efficient CPA Attack on Hardware Implementation of ML-DSA in Post-Quantum Root of Trust, IACR ePrint 2025/009; IEEE International Symposium on Hardware Oriented Security and Trust (HOST) 2025

    work page 2025

  8. [8]

    Adams Bridge

    Saarinen, Why “Adams Bridge” Leaks: Attacking a PQC Root-of-Trust, Hardwear.io USA 2025 (invited talk). Slides: https://hardwear.io/usa-2025/presentation/attacking- a-pqc-root-of-trust.pdf

    work page 2025

  9. [9]

    Module-Lattice-Based Digital Signature Standard (ML-DSA),

    National Institute of Standards and Technology, Module-Lattice-Based Digital Signature Standard, Federal Information Processing Standards Publication 204, August 13, 2024. DOI: 10.6028/NIST.FIPS.204

    work page doi:10.6028/nist.fips.204 2024

  10. [10]

    title Post-quantum cryptography standards: FIPS 203, 204, 205

    National Institute of Standards and Technology, Module-Lattice-Based Key- Encapsulation Mechanism Standard, Federal Information Processing Standards Publication 203, August 13, 2024. DOI: 10.6028/NIST.FIPS.203

    work page doi:10.6028/nist.fips.203 2024

  11. [11]

    Ishai, Sahai, Wagner, Private Circuits: Securing Hardware against Probing Attacks, CRYPTO 2003, LNCS 2729, pp. 463–481. Springer. DOI: 10.1007/978-3-540- 45146-4_27

    work page doi:10.1007/978-3-540- 2003

  12. [12]

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

    Barthe, G., Belaïd, S., Dupressoir, F., Fouque, P.-A., Grégoire, B., Strub, P.-Y., Zucchini, R. Strong Non-Interference and Type-Directed Higher-Order Masking. Proc. 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS ’16), Vienna, October 2016, ACM. DOI: 10.1145/2976749.2978427. ePrint 2015/506. 29

    work page doi:10.1145/2976749.2978427 2016

  13. [13]

    15 (2020), pp

    Cassiers, G., Standaert, F.-X., Trivially and Efficiently Composing Masked Gadgets with Probe Isolating Non-Interference, IEEE Transactions on Information Forensics and Security, Vol. 15 (2020), pp. 2542–2555. DOI: 10.1109/TIFS.2020.2971153. Preprint: IACR ePrint 2018/438

    work page doi:10.1109/tifs.2020.2971153 2020

  14. [14]

    doi:10.6028/NIST.FIPS.140-3 , url=

    National Institute of Standards and Technology, Security Requirements for Cryptographic Modules, Federal Information Processing Standards Publication 140-3, approved March 22, 2019; effective September 22, 2019. DOI: 10.6028/NIST.FIPS.140-3. URL: https://csrc.nist.gov/pubs/fips/140-3/final

    work page doi:10.6028/nist.fips.140-3 2019

  15. [15]

    National Institute of Standards and Technology, Transition to Post-Quantum Cryptography Standards, NIST Internal Report 8547 (Initial Public Draft), November

    work page

  16. [16]

    DOI: 10.6028/NIST.IR.8547.ipd

    work page doi:10.6028/nist.ir.8547.ipd

  17. [17]

    International Organization for Standardization / International Electrotechnical Commission, Information technology – Security techniques – Testing methods for the mitigation of non-invasive attack classes against cryptographic modules, ISO/IEC 17825:2024

    work page 2024

  18. [18]

    Barthe, Belaïd, Dupressoir, Fouque, Grégoire, Strub, Verified Proofs of Higher-Order Masking, EUROCRYPT 2015, LNCS 9056, pp. 457–485. Springer. DOI: 10.1007/978-3-662-46800-5_18. Preprint: IACR ePrint 2015/060

    work page doi:10.1007/978-3-662-46800-5_18 2015

  19. [19]

    Knichel, Sasdrich, Moradi, SILVER – Statistical Independence and Leakage Verification, ASIACRYPT 2020 (ePrint 2020/634)

    work page 2020

  20. [20]

    Higher Order Masking of Look-Up Tables

    Coron, J.-S. Higher Order Masking of Look-Up Tables. EUROCRYPT 2014, LNCS 8441, pp. 441–458. DOI: 10.1007/978-3-642-55220-5_25. ePrint 2013/700

    work page doi:10.1007/978-3-642-55220-5_25 2014

  21. [21]

    A Sound Method for Switching between Boolean and Arithmetic Masking

    Goubin, L. A Sound Method for Switching between Boolean and Arithmetic Masking. CHES 2001, LNCS 2162, pp. 3–15. Springer. DOI: 10.1007/3-540-44709-1_2

    work page doi:10.1007/3-540-44709-1_2 2001

  22. [22]

    In: Proc

    Coron, J.-S., Tchulkine, A. A New Algorithm for Switching from Arithmetic to Boolean Masking. CHES 2003, LNCS 2779, pp. 89–97. Springer. DOI: 10.1007/978- 3-540-45238-6_8

    work page doi:10.1007/978- 2003

  23. [23]

    Adams Bridge Accelerator: Bridging the Post-Quantum Transition

    Bisheh-Niasar, M., Karabulut, E., Upadhyayula, K., Norris, M., Pillilli, B. Adams Bridge Accelerator: Bridging the Post-Quantum Transition. IACR ePrint 2026/256. (Design paper for the Caliptra-family Adams Bridge accelerator; distinct in both authorship and substance from [8]. Identity-disambiguation note: this entry’s second author is Emre Karabulut (Cal...

    work page 2026

  24. [24]

    Adams Bridge: An Accelerator for Post-Quantum Resilient Cryptography, Microsoft Azure Confidential Computing Blog, October 15, 2024

    Pillilli, B., et al. Adams Bridge: An Accelerator for Post-Quantum Resilient Cryptography, Microsoft Azure Confidential Computing Blog, October 15, 2024. Announcement of the open-sourced Adams Bridge accelerator (ML-DSA / Dilithium only) as a discrete crypto accelerator and as integrated into Caliptra 2.0. URL: https://techcommunity.microsoft.com/blog/azu...

    work page arXiv 2024

  25. [25]

    Integrates Adams Bridge 2.0 with both ML-DSA-87 and ML-KEM 1024 and side-channel countermeasures

    CHIPS Alliance, Caliptra 2.1 RTL Release, October 2025 (announced at OCP Global Summit). Integrates Adams Bridge 2.0 with both ML-DSA-87 and ML-KEM 1024 and side-channel countermeasures. URL: 30 https://www.chipsalliance.org/news/caliptra2-1/; release notes at https://github.com/chipsalliance/caliptra-rtl/blob/main/Release_Notes.md

    work page 2025

  26. [26]

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

    Groß, H., Mangard, S., Korak, T. Domain-Oriented Masking: Compact Masked Hardware Implementations with Arbitrary Protection Order. Proceedings of the 2016 ACM Workshop on Theory of Implementation Security (TIS ’16), pp. 3–13, October

    work page 2016

  27. [27]

    Preprint: IACR ePrint 2016/486

    DOI: 10.1145/2996366.2996426. Preprint: IACR ePrint 2016/486

    work page doi:10.1145/2996366.2996426 2016

  28. [28]

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

    Faust, S., Grosso, V., Merino Del Pozo, S., Paglialonga, C., Standaert, F.-X. Composable Masking Schemes in the Presence of Physical Defaults & the Robust Probing Model. IACR Transactions on Cryptographic Hardware and Embedded Systems (TCHES), 2018(3), pp. 89–120. DOI: 10.13154/tches.v2018.i3.89-120. Preprint: IACR ePrint 2017/711

    work page doi:10.13154/tches.v2018.i3.89-120 2018