pith. sign in

arxiv: 2604.25878 · v2 · submitted 2026-04-28 · 💻 cs.CR

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

Ray Iskander , Khaled Kirah This is my paper

Pith reviewed 2026-05-08 03:24 UTC · model grok-4.3

classification 💻 cs.CR
keywords arithmetic maskingprime-field PININTTpost-quantum cryptographycomposition theoremsformal verificationLean 4Barrett reduction
0
0 comments X

The pith

Fresh random masks between arithmetic stages erase earlier security parameters in prime-field PINI for NTT masking.

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

The paper establishes the first machine-checked composition theorems for arithmetic masking over prime fields, the basis of NTT operations in post-quantum cryptography. It introduces the renewal argument showing that a fresh random mask inserted between two PF-PINI gadgets renders the intermediate wire perfectly uniform, so the composed pipeline meets PF-PINI security only at the level of the second gadget's parameter k2. A sympathetic reader would care because prior work had no analogous theory for arithmetic masking, leaving hardware designers without formal rules to compose masked operations securely. The result directly diagnoses that missing fresh masking in real accelerators creates non-uniform wires that retain multiplicity from the first stage, a necessary condition for differential power analysis.

Core claim

For any two PF-PINI gadgets with parameters k1 and k2, the two-stage pipeline formed by composing them with a fresh random mask between stages satisfies PF-PINI(k2), and Stage 1's multiplicity is erased from the composed output. The proof proceeds by showing that the fresh mask forces the intermediate value to be independent of all prior computations under the probing model.

What carries the argument

The renewal argument: inserting a fresh random mask between pipeline stages produces an intermediate wire that is perfectly uniform and independent of the preceding gadget's security parameter.

If this is right

  • Composed NTT designs achieve security determined solely by the final stage once fresh inter-stage masking is present.
  • Absence of fresh masking leaves intermediate wires with multiplicity up to k1, creating a necessary condition for first-order differential power analysis.
  • The Adams Bridge accelerator's Barrett outputs are formally non-uniform under the first-order probing model because it lacks fresh inter-stage masking.
  • Computational checks indicate the same 1-bit barrier appears in both Barrett and Montgomery reductions.

Where Pith is reading between the lines

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

  • Hardware implementations of NTT-based post-quantum crypto should incorporate dedicated random-mask generation logic between pipeline stages to satisfy the composition theorems.
  • The same renewal approach may apply to higher-order or multi-stage pipelines if uniformity can be re-established at each boundary.
  • Formal verification tools like Lean 4 can now be used to certify concrete accelerator designs against leakage before tape-out.

Load-bearing premise

The renewal argument assumes that a fresh random mask produces a perfectly uniform intermediate wire independent of prior stage computations under the chosen probing model and the hardware-faithful representation of operations such as Barrett reduction.

What would settle it

A statistical test on the output distribution of a two-stage masked pipeline that shows the final wires remain dependent on the first-stage masks even after fresh masking would falsify the renewal claim.

Figures

Figures reproduced from arXiv: 2604.25878 by Khaled Kirah, Ray Iskander.

Figure 1
Figure 1. Figure 1: The verification stack. Sections 4–5 prove composition theorems at the algebraic level (ZMod q). Theorem 6.1 bridges to hardware-faithful Nat arithmetic. The Nat-to-RTL step is supported by standard synthesis tools. Our formal bridge covers the mathematically subtle middle layer, the algebraic-to-Nat correspondence. The Nat-to-RTL step is well-understood and supported by standard synthesis tools (e.g., Yos… view at source ↗
read the original abstract

This is Paper 6 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. Boolean masking composition is well-understood through NI, SNI, and PINI. Arithmetic masking over $\mathbb{Z}_q$ for prime $q$, the foundation of NTT-based post-quantum cryptography, has lacked an analogous theory. We prove, to our knowledge, the first machine-checked composition theorems for arithmetic masking over prime fields. Our key insight is the renewal argument: when a fresh random mask is applied between two pipeline stages, the intermediate wire becomes perfectly uniform regardless of Stage 1's security parameter. For two PF-PINI gadgets with parameters $k_1$ and $k_2$, the composed two-stage pipeline with fresh masking satisfies PF-PINI($k_2$), Stage 1's multiplicity is completely erased from the composed output. Without fresh masking, intermediate wires have multiplicity up to $k_1$, creating a necessary condition for differential power analysis. We formalize both theorems in Lean 4 with 18 machine-checked proofs and zero sorry stubs. We formally bridge the algebraic and hardware-faithful arithmetic models of Barrett reduction, and instantiate the theorems to formally diagnose Microsoft's Adams Bridge PQC accelerator: its absence of fresh inter-stage masking leaves Barrett output wires non-uniform under the first-order probing model, the same architectural flaw that two independent empirical analyses [3, 4] and our own prior structural analysis [1] identified. Computational evidence further suggests the 1-Bit Barrier is universal across Barrett and Montgomery reductions.

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 manuscript introduces Prime-Field PINI (PF-PINI) as an arithmetic-masking analogue to Boolean PINI for post-quantum NTT hardware. It proves composition theorems for two-stage pipelines: for PF-PINI gadgets with parameters k1 and k2, fresh inter-stage masking yields a composed circuit satisfying PF-PINI(k2) because the renewal argument renders the intermediate wire perfectly uniform and erases Stage-1 multiplicity. Both theorems are formalized in Lean 4 with 18 machine-checked proofs (zero sorry stubs). The paper also supplies a formal bridge between the algebraic model and hardware-faithful arithmetic representations of Barrett reduction, then instantiates the theorems to diagnose the absence of fresh masking in Microsoft's Adams Bridge accelerator, confirming non-uniform Barrett output wires under the first-order probing model.

Significance. If the results hold, the work is significant because it supplies the first machine-checked composition theory for prime-field arithmetic masking, directly addressing a gap in post-quantum cryptography hardware security. The 18 zero-sorry Lean proofs, the explicit formalization of the renewal argument, and the bridge to hardware-faithful Barrett reduction provide strong internal verification and practical diagnostic power. The concrete application to an existing accelerator, cross-referenced with prior empirical and structural analyses, adds immediate engineering value.

minor comments (2)
  1. The abstract and introduction refer to the work as 'Paper 6 of a series' without a concise one-paragraph recap of the prior results (structural dependency analysis and partial-masking margins) that are presupposed by the current theorems; adding such a recap would improve accessibility for readers outside the series.
  2. Notation for the probing model and the exact definition of 'multiplicity' on intermediate wires is introduced inline in the theorems but would benefit from a dedicated preliminary subsection or table that lists all model parameters and their Lean encodings.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive review, accurate summary of our contributions, and recommendation to accept the manuscript. The assessment correctly identifies the novelty of the machine-checked PF-PINI composition theorems, the renewal argument, the Lean 4 formalization with zero sorry stubs, and the diagnostic application to the Adams Bridge accelerator.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's derivation consists of 18 machine-checked Lean 4 proofs (zero sorry stubs) establishing the PF-PINI composition theorems and the renewal argument that fresh masking erases Stage-1 multiplicity by rendering the intermediate wire uniform. These proofs operate within a formal system that explicitly bridges the algebraic model to the hardware-faithful arithmetic representation of Barrett reduction. Self-citations to prior series papers supply only contextual background on QANARY and partial masking; they are not invoked as load-bearing uniqueness theorems or ansatzes. The central claims therefore reduce to independently verifiable formal statements rather than to fitted parameters, self-definitions, or unverified self-citations.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper relies on standard mathematical properties of prime fields and uniform randomness for the uniformity claims, with the main contribution being the formalization of new composition theorems rather than new axioms or entities.

axioms (1)
  • standard math Standard algebraic properties of prime fields and uniform distribution of fresh random masks
    Invoked to establish that fresh masking produces perfect uniformity independent of prior stage outputs.
invented entities (1)
  • PF-PINI no independent evidence
    purpose: Security notion capturing probing-isolated non-interference for prime-field arithmetic masking
    Newly introduced definition to state and prove the composition theorems.

pith-pipeline@v0.9.0 · 5621 in / 1282 out tokens · 65028 ms · 2026-05-08T03:24:02.451716+00:00 · methodology

Review history (2 revisions) →

discussion (0)

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

Forward citations

Cited by 1 Pith paper

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

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

Reference graph

Works this paper leans on

17 extracted references · 5 canonical work pages · cited by 1 Pith paper · 5 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 Number Theoretic Transform masking in post-quantum cryptography (PQC) hardware: A security margin analysis”, arXiv:2604.03813, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  3. [3]

    Efficient CPA attack on hardware implementation of ML-DSA in post-quantum root of trust

    M. Karabulut and R. Azarderakhsh, “Efficient CPA attack on hardware implementation of ML-DSA in post-quantum root of trust”, IACR ePrint 2025/009, 2025

    2025

  4. [4]

    Why Adams Bridge leaks: Attacking a PQC root -of-trust

    M.-J. O. Saarinen , “Why Adams Bridge leaks: Attacking a PQC root -of-trust”, Hardwear.io USA, 2025

    2025

  5. [5]

    Ishai, A

    Y. Ishai, A. Sahai, and D. Wagner. Private circuits: Securing hardware against probing attacks. In CRYPTO 2003, LNCS 2729, pp. 463–481. Springer, 2003

    2003

  6. [6]

    Strong non -interference and type -directed higher -order masking

    G. Barthe, S. Belaïd, F. Dupressoir, P. -A. Fouque, B. Grégoire, P. -Y. Strub, and R. Zucchini, “Strong non -interference and type -directed higher -order masking ”, In ACM CCS 2016, pp. 116–129, 2016

    2016

  7. [7]

    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, 15:2542–2555, 2020

    2020

  8. [8]

    Verified proofs of higher-order masking

    G. Barthe, S. Belaïd, F. Dupressoir, P.-A. Fouque, B. Grégoire, and P.-Y. Strub, “Verified proofs of higher-order masking”, In EUROCRYPT 2015, LNCS 9056, pp. 457–485. Springer, 2015

    2015

  9. [9]

    maskVerif: Automated verification of higher -order masking in presence of physical defaults

    G. Barthe, S. Belaïd, G. Cassiers, P. -A. Fouque, B. Grégoire, and F. -X. Standaert , “maskVerif: Automated verification of higher -order masking in presence of physical defaults”, In ESORICS 2019, LNCS 11735, pp. 300–318. Springer, 2019

    2019

  10. [10]

    SILVER – Statistical independence and leakage verification

    D. Knichel, P. Sasdrich, and A. Moradi , “SILVER – Statistical independence and leakage verification”, In ASIACRYPT 2020, LNCS 12491, pp. 787–816. Springer, 2020

    2020

  11. [11]

    Coco: Co-design and co- verification of masked software implementations on CPUs

    B. Gigerl, V. Hadžić, R. Primas, S. Mangard, and R. Bloem , “Coco: Co-design and co- verification of masked software implementations on CPUs ”, In USENIX Security 2021 , pp. 1469–1486, 2021

    2021

  12. [12]

    Secure conversion between Boolean and arithmetic masking of any order

    J.-S. Coron, J. Großschädl, and P. K. Vadnala, “Secure conversion between Boolean and arithmetic masking of any order”, In CHES 2014, LNCS 8731, pp. 188–205. Springer, 2014

    2014

  13. [13]

    Conversion from arithmetic to Boolean masking with logarithmic complexity

    J.-S. Coron, J. Großschädl, M. Tibouchi, and P. K. Vadnala , “ Conversion from arithmetic to Boolean masking with logarithmic complexity ”, In FSE 2015 , LNCS 9054, pp. 130–149. Springer, 2015

    2015

  14. [14]

    Adams Bridge: Post-quantum cryptographic accelerator

    Chipsalliance. Adams Bridge: Post-quantum cryptographic accelerator. GitHub, 2024

    2024

  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

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  16. [16]

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

    R. Iskander and K. Kirah , “ Fresh masking makes NTT pipelines composable ”, arXiv:2604.20793, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  17. [17]

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

    R. Iskander and K. Kirah , “Machine-checked cardinality bounds for masked Barrett reduction: A 1 -bit side -channel leakage barrier in post -quantum cryptographic hardware ”, Preprint, 2026. Available at https://github.com/rayiskander2406/qanary-one-bit-barrier- arXiv-2604.24670, 2026 Appendix A: Complete Lean 4 Proof Listing The complete proof suite cons...

    work page internal anchor Pith review Pith/arXiv arXiv 2026