pith. sign in

arxiv: 2604.24670 · v2 · submitted 2026-04-27 · 💻 cs.CR

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

Ray Iskander , Khaled Kirah This is my paper

Pith reviewed 2026-05-08 02:41 UTC · model grok-4.3

classification 💻 cs.CR
keywords Barrett reductionarithmetic maskingside-channel leakagemachine-checked proofpost-quantum cryptographycardinality boundprime field
0
0 comments X

The pith

Masked Barrett reduction leaks at most one bit per internal wire

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

The paper proves a trichotomy for the Barrett reduction map used in post-quantum cryptography: for any modulus and shift, each possible output has either zero, one, or two possible inputs. This limits the information leaked through each wire to at most one bit when arithmetic masking is applied. The proof covers all positive moduli and is verified by a computer in the Lean 4 language with no unproven steps. They also introduce a notion of security for prime-field masking and apply it to the reduction and butterfly operations. This establishes a universal leakage barrier for masked implementations.

Core claim

For any q greater than zero and any shift s, the Barrett internal wire map has preimage cardinality always in the set containing zero, one, or two. This 1-Bit Barrier implies at most one bit of min-entropy loss per internal wire. The reduction satisfies the prime-field security property at level two while the butterfly satisfies it at level one. The trichotomy, the security properties, and the cardinality results are all machine-checked in Lean 4 with zero unproven steps and hold for every positive modulus.

What carries the argument

The trichotomy on preimage cardinalities of the Barrett map, which bounds information leakage under arithmetic masking to at most one bit per wire.

Load-bearing premise

Composing masked stages with fresh masking between them will not increase the maximum number of inputs that map to one output beyond what each stage allows.

What would settle it

A specific choice of modulus q, shift s, and input x where the Barrett map has three or more different m values producing the same output, or a simulation of a masked circuit that extracts more than one bit of information.

read the original abstract

Barrett reduction is the nonlinear core of every practical NTT-based post-quantum cryptography implementation. Existing composition frameworks (ISW, t-SNI, PINI, DOM) address Boolean masking over GF(2); none provides a machine-checked characterization of Barrett's leakage under first-order arithmetic masking and the first-order probing model over prime fields. Building on our prior series, QANARY [15], partial-NTT-masking margins [14], algebraic foundations [16], and butterfly composition [18], we close this gap. We prove a trichotomy: for any $q > 0$ and shift $s$, the Barrett internal wire map $f_x(m) = ((x + 2^s - m) \bmod 2^s) \bmod q$ has preimage cardinality in $\{0, 1, 2\}$, never more. We call this the 1-Bit Barrier: max-multiplicity 2 implies at most 1 bit of min-entropy loss per internal wire, universal over all moduli. The count-zero cases, unreachable output values, reveal that actual leakage is often strictly less than 1 bit, making the bound conservative. We introduce PF-PINI (Prime-Field PINI): Barrett satisfies PF-PINI(2); the Cooley-Tukey butterfly satisfies PF-PINI(1). We observe (not yet proved) that with fresh inter-stage masking, the composed pipeline has max-multiplicity $\max(k_1, k_2)$, so the 1-Bit Barrier propagates. The trichotomy, the PF-PINI instantiations, and cardinality results are machine-checked in Lean 4 with Mathlib: 12 proved results, zero sorry, universal over all $q > 0$ (the min-entropy bound follows by standard definitions). Adams Bridge lacks fresh inter-stage masking, violating PF-PINI composition and explaining why Papers 1 [15] and 2 [14] found vulnerabilities. NIST IR 8547 recommends formal methods for PQC implementation validation. The 1-Bit Barrier provides the first universal machine-checked cardinality bound for masked Barrett reduction in ML-KEM (FIPS 203) and ML-DSA (FIPS 204), with a corresponding 1-bit leakage interpretation.

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 paper claims to establish the first universal machine-checked cardinality bounds for masked Barrett reduction under first-order arithmetic masking in the probing model. It proves a trichotomy: for any q > 0 and shift s, the Barrett internal wire map f_x(m) = ((x + 2^s - m) mod 2^s) mod q has preimage cardinality in {0, 1, 2}. It introduces the PF-PINI notion, proves PF-PINI(2) for Barrett and PF-PINI(1) for the Cooley-Tukey butterfly, and observes that fresh inter-stage masking composes these to preserve max-multiplicity max(k1, k2), yielding at most 1 bit of min-entropy loss per wire in a full masked NTT pipeline for ML-KEM/ML-DSA. All core results (trichotomy, PF-PINI instantiations, cardinality) are formalized in Lean 4 with 12 theorems and zero sorries.

Significance. If the composition observation is formalized, the result would be significant: it supplies the first parameter-free, machine-checked leakage bound that is universal over all moduli q, directly applicable to the nonlinear core of every NTT-based PQC implementation. The explicit credit for 12 proved Lean theorems against standard definitions of preimage cardinality and min-entropy, together with the conservative nature of the bound (count-zero cases often yield strictly less than 1 bit), strengthens its value for NIST-recommended formal validation of masked hardware.

major comments (1)
  1. [Abstract / pipeline composition] Abstract and § on pipeline composition: the claim that the 1-Bit Barrier propagates to the full masked NTT pipeline rests on the unproved observation that 'with fresh inter-stage masking, the composed pipeline has max-multiplicity max(k1, k2)'. This is load-bearing for the central universal leakage guarantee; without a theorem establishing preservation of the multiplicity bound under the concrete arithmetic maps and fresh masking, higher multiplicity (and thus >1 bit leakage) remains possible even when each stage individually satisfies its PF-PINI bound.
minor comments (1)
  1. [Abstract] The manuscript refers to 'Papers 1 [15] and 2 [14]' for Adams Bridge vulnerabilities; explicit section numbers or theorem references in those works would improve traceability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for recognizing the significance of the machine-checked trichotomy and PF-PINI results. We agree that the pipeline composition claim requires clarification and will revise the manuscript to address this.

read point-by-point responses

  1. Referee: [Abstract / pipeline composition] Abstract and § on pipeline composition: the claim that the 1-Bit Barrier propagates to the full masked NTT pipeline rests on the unproved observation that 'with fresh inter-stage masking, the composed pipeline has max-multiplicity max(k1, k2)'. This is load-bearing for the central universal leakage guarantee; without a theorem establishing preservation of the multiplicity bound under the concrete arithmetic maps and fresh masking, higher multiplicity (and thus >1 bit leakage) remains possible even when each stage individually satisfies its PF-PINI bound.

    Authors: We agree that the composition property is currently an observation rather than a machine-checked theorem, as the manuscript already states: 'We observe (not yet proved)'. The PF-PINI definition is constructed so that fresh, independent arithmetic masks between stages reset the multiplicity bound to the maximum of the per-component bounds; this follows directly from the uniform randomness of each fresh mask and the fact that preimage cardinalities do not accumulate across independent masks. This mirrors standard composition arguments in the PINI literature. To meet the referee's concern, the revised manuscript will either add a Lean 4 formalization of the composition theorem or explicitly qualify the full-pipeline claim as conditional on the fresh-masking assumption, while leaving the 12 proved theorems on the trichotomy, Barrett PF-PINI(2), and butterfly PF-PINI(1) unchanged. The abstract will be updated to reflect this distinction. revision: partial

Circularity Check

0 steps flagged

Lean-formalized trichotomy and PF-PINI with acknowledged unproved composition

full rationale

The paper's derivation chain consists of direct machine-checked Lean proofs (12 results, zero sorry) of the trichotomy on preimage cardinality of f_x(m) = ((x + 2^s - m) mod 2^s) mod q lying in {0,1,2} and the PF-PINI(2)/PF-PINI(1) properties for Barrett and butterfly. These are formalized against standard Mathlib definitions of cardinality and min-entropy with no reduction to author-fitted quantities, self-defined parameters, or prior results by construction. Self-citations to [15],[14],[16],[18] supply background on related masking work but are not load-bearing for the new cardinality bounds. The composition rule for fresh inter-stage masking is explicitly labeled an unproved observation rather than a derived claim, so the paper does not assert a circular derivation for the full pipeline. The result is therefore self-contained against external mathematical benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on standard properties of modular arithmetic and the newly introduced PF-PINI definition; no numerical parameters are fitted to data.

axioms (1)
  • standard math Standard properties of integer modular arithmetic and preimage cardinality
    Invoked throughout the trichotomy proof.
invented entities (1)
  • PF-PINI no independent evidence
    purpose: Prime-field analogue of probing security for arithmetic masking
    New definition introduced to state the security property satisfied by Barrett reduction.

pith-pipeline@v0.9.0 · 5737 in / 1348 out tokens · 77664 ms · 2026-05-08T02:41:28.018862+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 3 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.

Reference graph

Works this paper leans on

46 extracted references · 6 canonical work pages · cited by 2 Pith papers · 6 internal anchors

  1. [1]

    Abstract Barrett reduction is the nonlinear core of every practical NTT -based post -quantum cryptography implementation. Existing composition frameworks (ISW, t -SNI, PINI, DOM) address Boolean masking over GF(2); none provides a machine -checked characterization of Barrett’s leakage under first-order arithmetic masking and the first -order probing model...

  2. [2]

    The NTT is implemented as a pipeline of Cooley -Tukey butterfly stages, each individually protected by first -order arithmetic masking with a fresh random mask

    Introduction Consider a hardware engineer designing a masked ML -KEM accelerator for FIPS 203 certification [5]. The NTT is implemented as a pipeline of Cooley -Tukey butterfly stages, each individually protected by first -order arithmetic masking with a fresh random mask. Between the butterfly stages, 2 Barrett reduction performs modular reduction, the s...

  3. [3]

    The Barrett internal wire map has preimage cardinality in {0,1,2}, universal over all 𝑞 > 0 and all shift parameters 𝑠

    The trichotomy theorem. The Barrett internal wire map has preimage cardinality in {0,1,2}, universal over all 𝑞 > 0 and all shift parameters 𝑠. Machine-checked in Lean 4 with zero sorry. 3

  4. [4]

    Max-multiplicity 2 implies 𝐻∞(output ∣ 𝑥) ≥ log2(𝑞) − 1 per internal wire

    The 1 -Bit Barrier. Max-multiplicity 2 implies 𝐻∞(output ∣ 𝑥) ≥ log2(𝑞) − 1 per internal wire. For ML -KEM ( 𝑞 = 3329): 𝐻∞ ≥ 10.70 bits. For ML -DSA ( 𝑞 = 8,380,417): 𝐻∞ ≥ 21.99 bits

  5. [5]

    Barrett satisfies PF-PINI(2)

    The PF-PINI framework. Barrett satisfies PF-PINI(2). The identity masking gadget (modeling butterfly output wires) satisfies PF -PINI(1). We observe (not yet proved) that with fresh inter -stage masking, a composed pipeline has max -multiplicity max(𝑘1, 𝑘2), the 1-Bit Barrier propagates. 2.5. Honest scope The trichotomy proof is clean because of the two -...

  6. [6]

    The NTT butterfly is affine in the mask. Composition for nonlinear gadgets such as Barrett reduction remains future work

    Background 3.1. Barrett Reduction in PQC Hardware Barrett reduction computes 𝑥 mod 𝑞 for an integer 𝑥 using precomputed constants, avoiding expensive division. The algorithm: multiply by an approximation 𝜇 = ⌊2𝑠/𝑞⌋, shift right by 𝑠, multiply by 𝑞, subtract, and apply one conditional correction. Table 1 lists the parameters used in Adams Bridge [13]. Para...

  7. [7]

    Related Work 4.1. Comparison with Prior Work Table 2 summarizes how prior masking-verification approaches relate to this work along five axes: target masking model, Barrett -specific coverage, universality of the bound, machine - checked status, and PF-PINI applicability. Framework Venue Masking Barrett Universal Machine- Checked PF-PINI ISW [6] CRYPTO 20...

    2003

  8. [8]

    The Trichotomy Theorem This section contains the mathematical heart of the paper. 5.1. The Barrett Internal Wire Map We define the Barrett internal wire map algebraically using the two-branch structure observed in hardware. For any 𝑞 > 0, shift parameter 𝑠, secret 𝑥 ∈ ℤ𝑞, and mask 𝑚 ∈ ℤ𝑞: 𝑓𝑥(𝑚) = {𝑥 − 𝑚 if 𝑚.val ≤ 𝑥.val 𝑥 − 𝑚 + 𝑟 otherwise where 𝑟 = (2𝑠: ...

  9. [9]

    Support-gap structure of the Barrett internal wire map for selected secrets in ML - KEM ( 𝑞 = 3329, 𝑠 = 24, 𝑟 = 2385)

    Doubled values (count = 2) 0 1 1 100 101 101 832 (≈ 𝑞/4) 833 833 1664 (≈ 𝑞/2) 944 944 2496 (≈ 3𝑞/4) 832 832 3327 (𝑞 − 2) 1 1 3328 (𝑞 − 1) 0 (bijective) 0 Table 3. Support-gap structure of the Barrett internal wire map for selected secrets in ML - KEM ( 𝑞 = 3329, 𝑠 = 24, 𝑟 = 2385). The unreachable count equals the doubled count by conservation. At 𝑥 = 𝑞 − ...

  10. [10]

    Max Output Probability The max-multiplicity bound directly implies a probability bound

    The 1-Bit Barrier Security Consequence 6.1. Max Output Probability The max-multiplicity bound directly implies a probability bound. Definition. The max output probability for secret 𝑥 and output 𝑣 is: Pr[output = 𝑣 ∣ secret = 𝑥] = |{𝑚 ∈ ℤ𝑞: 𝑓𝑥(𝑚) = 𝑣}| 𝑞 since each of the 𝑞 equally-likely masks contributes equally. Observation 5.1 (Max output probability ...

  11. [11]

    The PF-PINI Definition We define Prime -Field PINI (PF -PINI) as a direct preimage multiplicity bound for gadgets operating over ℤ𝑞

    Prime-Field PINI 7.1. The PF-PINI Definition We define Prime -Field PINI (PF -PINI) as a direct preimage multiplicity bound for gadgets operating over ℤ𝑞. Definition 6.1 (PF-PINI Gadget). An PF-PINI gadget over ℤ𝑞 is a structure consisting of: - A compute function 𝐺: ℤ𝑞 × ℤ𝑞 → ℤ𝑞 mapping (secret, mask) to wire value - A max-multiplicity parameter 𝑘 ∈ ℕ - ...

  12. [12]

    Intra-stage failure (Papers 1 and 2)

    Adams Bridge Connection 8.1 Two Distinct Failure Modes Adams Bridge [13] has two independent failure modes, now formally characterized across the five-paper program. Intra-stage failure (Papers 1 and 2). Within each NTT stage, both shares interact through combinational logic without fresh intermediate masking. QANARY’s structural dependency analysis [1] d...

  13. [13]

    Using fresh per -stage masking between NTT butterfly and Barrett stages (Paper 4’s Fresh Masking Design Principle [4])

  14. [14]

    Ensuring 𝑠 ≥ ⌈log2𝑞⌉ (trivially satisfied by all standard Barrett implementations)

  15. [15]

    Adams Bridge satisfies condition (2) but violates condition (1)

    Accepting 1 bit of worst-case internal leakage per Barrett wire. Adams Bridge satisfies condition (2) but violates condition (1). That is the architectural root cause of its vulnerabilities across the five-paper program

  16. [16]

    Proof Suite Summary Table 5 enumerates every theorem and verified construction in the Lean 4 artifact accompanying this paper. # Theorem File Key Technique Sorry-Free Closes 1 barrettIntern alMap_eq_o r Basic unfold + split Yes Two-branch structure 2 barrettIntern alMap_mem _pair Basic eq_or case split + linear_comb ination Yes Preimage characterizat ion ...

  17. [17]

    Limitations and Future Work We state all limitations explicitly. 10.1. (i) Support gap formula not proved The zero -multiplicity region size, min(𝑥.val + 1, 𝑞 − 𝑟, 𝑞 − 1 − 𝑥.val) where 𝑟 = 2𝑠 mod 𝑞, is computationally verified across 14 primes (including all PQC standard moduli: 𝑞 = 3329, 𝑞 = 8,380,417, 𝑞 = 7681, 𝑞 = 4591, 𝑞 = 12289) but is not a proved L...

  18. [18]

    The trichotomy

    Conclusion We have proved three machine -checked results for arithmetic masking in Barrett reduction, formalized in Lean 4 with Mathlib, with zero sorry. The trichotomy. The Barrett internal wire map has preimage cardinality in {0,1,2}, universal over all 𝑞 > 0 and all shift parameters 𝑠. The bound is tight: count = 2 is achievable. The count-zero cases r...

  19. [19]

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

    Code and Data Availability The Lean 4 artifact accompanying this paper is publicly available under the MIT license: • Repository: https://github.com/rayiskander2406/qanary-one-bit- barrier-arXiv-2604.24670 (arXiv ID will be substituted post-submission per series convention) • Toolchain: Lean 4 v4.30.0-rc1 (managed via elan) • Pinned dependency: Mathlib at...

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

  20. [20]

    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, April

    work page internal anchor Pith review Pith/arXiv arXiv

  21. [21]

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

    Zenodo: 10.5281/zenodo.19625392. GitHub: rayiskander2406/qanary-structural- dependency-analysis-arXiv-2604.15249. (Paper 1 in this series.)

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

  22. [22]

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

    R. Iskander and K. Kirah, “Partial NTT Masking in PQC Hardware: A Security Margin Analysis,” arXiv:2604.03813, April 2026. Zenodo: 10.5281/zenodo.19508454. GitHub: rayiskander2406/ntt-security-margins-arXiv-2604.03813. (Paper 2 in this series.) 22

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

  23. [23]

    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, April 2026. Zenodo: 10.5281/zenodo.19689480. GitHub: rayiskander2406/qanary-universal-masking- proofs-arXiv-2604.18717. (Paper 3 in this series.)

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

  24. [24]

    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: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware,” arXiv:2604.20793, April 2026. Zenodo: 10.5281/zenodo.19705450. GitHub: rayiskander2406/qanary-masked-ntt-pipeline- security-arXiv-2604.20793. (Paper 4 in this series.)

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

  25. [25]

    Module-Lattice-Based Key-Encapsulation Mechanism Standard,

    National Institute of Standards and Technology, “Module-Lattice-Based Key-Encapsulation Mechanism Standard,” NIST FIPS 203, August 2024

    2024

  26. [26]

    Private Circuits: Securing Hardware against Probing Attacks,

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

    2003

  27. [27]

    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 Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS ’16), ACM, 2016, pp. 116–129

    2016

  28. [28]

    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 Transactions on Information Forensics and Security , vol. 15, pp. 2542–2555, 2020

    2020

  29. [29]

    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,” in Proceedings of the ACM Workshop on Theory of Implementation Security (TIS@CCS ’16), ACM, 2016, pp. 3–14

    2016

  30. [30]

    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 Advances in Cryptology – EUROCRYPT 2015, LNCS 9056, Springer, 2015, pp. 457–485

    2015

  31. [31]

    SILVER – Statistical Independence and Leakage Verification,

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

    2020

  32. [32]

    CocoAlma: A Versatile Masking Verifier,

    V. Hadžić and R. Bloem, “CocoAlma: A Versatile Masking Verifier,” in Formal Methods in Computer-Aided Design (FMCAD), 2021

    2021

  33. [33]

    Adams Bridge – ML-DSA/ML-KEM Hardware Accelerator for Caliptra,

    CHIPS Alliance, “Adams Bridge – ML-DSA/ML-KEM Hardware Accelerator for Caliptra,” GitHub, 2024. Available: https://github.com/chipsalliance/adams-bridge

    2024

  34. [34]

    Z3: An Efficient SMT Solver,

    L. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS 4963, Springer, 2008, pp. 337–340

    2008

  35. [35]

    cvc5: A Versatile and Industrial-Strength SMT Solver,

    A. Barbosa, C. W. Barrett, M. Brain, et al., “cvc5: A Versatile and Industrial-Strength SMT Solver,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), LNCS 13243, Springer, 2022, pp. 415–442

    2022

  36. [36]

    The Lean 4 Theorem Prover and Programming Language,

    L. de Moura and S. Ullrich, “The Lean 4 Theorem Prover and Programming Language,” in Automated Deduction – CADE 28, LNCS 12699, Springer, 2021, pp. 625–635

    2021

  37. [37]

    The Lean Mathematical Library,

    The Mathlib Community, “The Lean Mathematical Library,” in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, pp. 367–381. 23

    2020

  38. [38]

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

    R. Bloem, H. Gross, R. Iusupov, B. Könighofer, S. Mangard, and J. Winter, “Formal Verification of Masked Hardware Implementations in the Presence of Glitches,” in Advances in Cryptology – EUROCRYPT 2018, LNCS 10821, Springer, 2018, pp. 321–353

    2018

  39. [39]

    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,” in Applied Cryptography and Network Security (ACNS 2023), LNCS 13905, Springer, 2023

    2023

  40. [40]

    eVer: Universal and Automated Verification of Side-Channel Security for Additive, Inner Product, Polynomial and General Code-Based Masking,

    M. Gourjon, M. Orlt, P. Pauls, and A. Treff, “eVer: Universal and Automated Verification of Side-Channel Security for Additive, Inner Product, Polynomial and General Code-Based Masking,” Cryptology ePrint Archive, Report 2026/208, 2026

    2026

  41. [41]

    Side Channel Cryptanalysis of a Higher Order Masking Scheme,

    J.-S. Coron, E. Prouff, and M. Rivain, “Side Channel Cryptanalysis of a Higher Order Masking Scheme,” in Cryptographic Hardware and Embedded Systems – CHES 2007, LNCS 4727, Springer, 2007, pp. 28–44

    2007

  42. [42]

    Module-Lattice-Based Digital Signature Standard,

    National Institute of Standards and Technology, “Module-Lattice-Based Digital Signature Standard,” NIST FIPS 204, August 2024

    2024

  43. [43]

    Formalization of the Polynomial Freiman-Ruzsa Conjecture in Lean 4,

    T. Tao, Y. Dillies, B. Mehta, et al., “Formalization of the Polynomial Freiman-Ruzsa Conjecture in Lean 4,” 2023. GitHub: teorth/pfr

    2023

  44. [44]

    Security Requirements for Cryptographic Modules,

    National Institute of Standards and Technology, “Security Requirements for Cryptographic Modules,” NIST FIPS 140-3, March 2019

    2019

  45. [45]

    Transition to Post-Quantum Cryptography Standards,

    National Institute of Standards and Technology, “Transition to Post-Quantum Cryptography Standards,” NIST IR 8547, November 2024

    2024

  46. [46]

    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,” Cryptology ePrint Archive, Report 2025/009, 2025

    2025