pith. sign in

arxiv: 2604.18717 · v2 · submitted 2026-04-20 · 💻 cs.CR

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

Ray Iskander , Khaled Kirah This is my paper

Pith reviewed 2026-05-10 04:02 UTC · model grok-4.3

classification 💻 cs.CR
keywords formal verificationpost-quantum cryptographymaskingLean 4theorem provingcommutative ringshardware securityside-channel analysis
0
0 comments X

The pith

Lean 4 proof establishes that value-independence implies identical marginal distributions for every modulus q

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

This paper delivers the first machine-checked universal proof in Lean 4 of the r-free sub-theorem of Theorem 3.9.1 from prior work on structural dependency analysis for masking. The theorem asserts that for any positive integer q, any wire function, and any pair of secrets, value-independence entails identical marginal output distributions. Earlier verification was limited to exhaustive checks at q equals 5, leaving applicability to the large q values in ML-KEM and ML-DSA unresolved. The new proof uses the axioms of the commutative ring Z/qZ to establish the result in five lines, reducing the trusted base from SMT solvers and scripts to the Lean kernel.

Core claim

The authors prove in Lean 4 that for every q greater than zero, every wire function, and every pair of secrets, value-independence implies identical marginal distributions. This is the r-free sub-theorem of Theorem 3.9.1. The formalization includes nine supporting theorems on reparametrization, bijectivity, overflow bounds, RNG bias, and a universal non-tightness counterexample for all q at least 2. The results establish the commutative ring axioms of Z/qZ as the natural abstraction layer for arithmetic masking verification.

What carries the argument

The r-free sub-theorem of Theorem 3.9.1, formalized in Lean 4 as the statement that value-independence of wire functions entails identical marginal distributions over the ring Z/qZ for arbitrary q.

Load-bearing premise

The arithmetic operations in PQC hardware masking implementations are accurately modeled by the commutative ring axioms of Z/qZ.

What would settle it

A concrete counterexample consisting of a wire function and secret pair for some q greater than 5 where value-independent wires produce different marginal distributions, as would be detected by hardware simulation or exhaustive enumeration.

Figures

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

Figure 1
Figure 1. Figure 1: Proof suite dependency structure. Solid arrows: logical dependency. Dashed [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
read the original abstract

Formal verification of masking in post-quantum cryptographic (PQC) hardware relies on SMT solvers over finite domains. Our prior work established structural dependency analysis at scale [1] and quantified the security margin of partial NTT masking [2]. QANARY, our structural dependency analysis framework, verified 1.17 million cells across 30 modules of the Adams Bridge ML-DSA/ML-KEM accelerator [3, 4], but its core soundness result (Theorem 3.9.1) was machine-checked only at $q = 5$ via $2^{25}$ Boolean wire functions. This left portability to ML-KEM ($q = 3{,}329$, FIPS 203 [5]) and ML-DSA ($q = 8{,}380{,}417$, FIPS 204 [6]) as an open gap. NIST IR 8547 [7] (March 2025) motivates closing such gaps. We present the first machine-checked universal proof of the $r$-free sub-theorem of Theorem 3.9.1: for every $q > 0$, every wire function, and every pair of secrets, value-independence implies identical marginal distributions. The proof, in Lean 4 [8] with Mathlib [9], requires five lines versus $2^{25}$ finite evaluations. It is sorry-free, reducing the trusted base from {Z3 [10], CVC5 [11], Python} to the Lean 4 kernel. We provide nine theorems (T1--T6, T1', T3') covering reparametrization, bijectivity, overflow bounds, RNG bias, and a universal non-tightness counterexample for all $q \geq 2$. The results establish commutative ring axioms of $\mathbb{Z}/q\mathbb{Z}$ as the natural abstraction layer for arithmetic masking verification.

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 presents the first machine-checked universal proof, in Lean 4 with Mathlib, of the r-free sub-theorem of Theorem 3.9.1: for every q > 0, every wire function, and every pair of secrets, value-independence implies identical marginal distributions. This replaces the prior 2^25 finite Boolean checks (limited to q=5) with a five-line sorry-free formalization that applies directly to the moduli of ML-KEM (q=3329) and ML-DSA (q=8380417). The work also supplies nine additional theorems (T1–T6, T1', T3') on reparametrization, bijectivity, overflow bounds, RNG bias, and a universal non-tightness counterexample, all derived from the commutative ring axioms of Z/qZ.

Significance. If the formalization holds, the result closes a critical portability gap for structural dependency analysis in PQC hardware masking verification. It reduces the trusted computing base from SMT solvers and Python scripts to the Lean 4 kernel, supplies a parameter-free ring-theoretic abstraction layer, and furnishes machine-checked evidence that value-independence is sufficient for identical marginals across all q > 0. The universal counterexample and auxiliary theorems further strengthen the framework’s applicability to real-world accelerators such as Adams Bridge.

minor comments (2)
  1. The abstract and §3 reference nine theorems (T1–T6, T1', T3') but the manuscript does not include a consolidated table or lemma numbering that maps each theorem to its Lean statement; adding such a cross-reference would improve readability.
  2. The discussion of the modeling assumption (Z/qZ as an accurate abstraction of hardware arithmetic) appears only in the abstract and conclusion; a short dedicated paragraph in §2 or §4 clarifying the precise correspondence between ring operations and masked wire functions would strengthen the bridge to implementation.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive review, the detailed summary of our contributions, and the recommendation to accept the manuscript. The assessment accurately captures the shift from finite Boolean enumeration to a universal ring-theoretic proof in Lean 4.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper's core result is a new, sorry-free Lean 4 formalization (five lines using Mathlib) of the r-free sub-theorem of Theorem 3.9.1, establishing value-independence implies identical marginal distributions for every q > 0. This is derived from standard commutative ring axioms of Z/qZ rather than from the prior finite enumeration at q=5 or any fitted parameters. Self-citations to prior works [1-4] supply only problem context and do not carry the load of the universal proof; the derivation chain remains independent of those empirical checks and reduces to the Lean kernel plus Mathlib. No self-definitional, fitted-input, or ansatz-smuggling patterns appear in the stated claims or proof description.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The proof relies on standard mathematical axioms from Mathlib and the definition of the ring structure, with no free parameters or new entities introduced.

axioms (1)
  • standard math Commutative ring axioms for Z/qZ
    Used as the abstraction layer for arithmetic masking verification as stated in the abstract.

pith-pipeline@v0.9.0 · 5648 in / 1119 out tokens · 29550 ms · 2026-05-10T04:02:39.063292+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 5 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. Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

    cs.CR 2026-04 accept novelty 8.0 full

    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.

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

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

47 extracted references · 47 canonical work pages · cited by 4 Pith papers · 4 internal anchors

  1. [1]

    NIST IR 8547, published in March 2025, establishes the transition timeline and recommends formal methods for validating PQC implementations

    Introduction The finalization of ML-KEM (FIPS 203) and ML-DSA (FIPS 204) in August 2024 marks the beginning of a large-scale migration to post-quantum cryptography. NIST IR 8547, published in March 2025, establishes the transition timeline and recommends formal methods for validating PQC implementations. For hardware accelerators implementing these standa...

    work page 2024

  2. [2]

    The proof requires five lines of tactic script (Section 4)

    A universal Lean 4 proof of the 𝑟-free sub-theorem of Theorem 3.9.1, valid for all 𝑞 > 0, all wire functions 𝑤: ℤ𝑞 × ℤ𝑞 → 𝛽 (for arbitrary output type 𝛽), and all secrets 𝑥, 𝑥′. The proof requires five lines of tactic script (Section 4). By the law of total probability, establishing this 𝑟-free algebraic property is the exact prerequisite for full probabi...

    work page

  3. [3]

    Universal proofs of six supporting theorems (T2 –T6): reparametrization round - trips for Boolean and arithmetic masking, reparametrization bijectivity, overflow bounds bridging to bit -vector implementations, RNG bias characterization, and a universal non-tightness counterexample showing that the converse of Theorem 3.9.1 fails for every 𝑞 ≥ 2 (Section 5)

    work page

  4. [4]

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

    A methodological insight: the five-line proof follows from commutative ring axioms alone (sub_add_cancel in Mathlib’s CommRing instance for ℤ/𝑞ℤ). The secret -mask reparametrization is a ring identity, not a computational procedure. This reveals that ring theory, not bit-vector SAT, is the natural abstraction layer for arithmetic masking verification (Sec...

    work page internal anchor Pith review Pith/arXiv arXiv

  5. [5]

    Arithmetic Masking in NTT Hardware First-order arithmetic masking splits a secret 𝑥 ∈ ℤ𝑞 into two shares 𝑠0, 𝑠1 ∈ ℤ𝑞 satisfying 𝑠0 + 𝑠1 ≡ 𝑥 (mod 𝑞)

    Background 2.1. Arithmetic Masking in NTT Hardware First-order arithmetic masking splits a secret 𝑥 ∈ ℤ𝑞 into two shares 𝑠0, 𝑠1 ∈ ℤ𝑞 satisfying 𝑠0 + 𝑠1 ≡ 𝑥 (mod 𝑞). An adversary observing a single wire (the standard probing model [13]) should learn nothing about 𝑥. Definition 1 (Wire Function). A wire function is a map 𝑤: ℤ𝑞 × ℤ𝑞 → 𝛽 where 𝛽 is an arbitra...

    work page

  6. [6]

    A wire depending only on 𝑠0 or only on 𝑠1 is trivially secure

    D0/D1 queries: for each wire, determine which shares influence its value. A wire depending only on 𝑠0 or only on 𝑠1 is trivially secure

    work page

  7. [7]

    Fresh masking (FM): identify wires protected by fresh randomness, which masks the dependence on the secret

    work page

  8. [8]

    Boolean SADC: for Boolean -masked domains, check value -independence via the XOR reparametrization

    work page

  9. [9]

    Theorem 3.9.1 is the soundness guarantee for stage 4: any wire that SADC labels SECURE (i.e., value-independent) provably leaks no information about the secret

    Arithmetic SADC: for arithmetic -masked domains (NTT butterflies, Barrett reduction), check value -independence via the modular subtraction reparametrization (Definition 2). Theorem 3.9.1 is the soundness guarantee for stage 4: any wire that SADC labels SECURE (i.e., value-independent) provably leaks no information about the secret. 2.3. The Finite-Domain...

    work page

  10. [10]

    SMT solvers cannot perform structural induction over 𝑞

    No induction. SMT solvers cannot perform structural induction over 𝑞. A proof at 𝑞 = 5 is logically independent of a proof at 𝑞 = 3,329

    work page

  11. [11]

    At 𝑞 = 3,329, the wire space has 233292 = 211,082,241 elements, far beyond feasible enumeration

    Exponential scaling. At 𝑞 = 3,329, the wire space has 233292 = 211,082,241 elements, far beyond feasible enumeration

    work page

  12. [12]

    Correctness depends on the absence of bugs in Z3, CVC5, and the Python encoding that generates the SMT-LIB2 queries

    Trusted base. Correctness depends on the absence of bugs in Z3, CVC5, and the Python encoding that generates the SMT-LIB2 queries. Paper 2 explicitly listed this finite -domain ceiling as the one remaining open methodological gap (Section 6, Limitation (ii)). This paper closes it. 2.4. Interactive Theorem Proving with Lean 4 Lean 4 is a dependently typed ...

    work page

  13. [13]

    Universal

    Related Work Table 1 summarizes the landscape. We distinguish three axes: the masking domain (Boolean vs. arithmetic), whether the result is universal over parameters, and whether the formalization targets NTT-specific hardware. Table 1. Comparison of formal masking verification approaches. “Universal” means the result holds for all parameter values (modu...

    work page 2015

  14. [14]

    Let 𝑞 > 0

    The Main Theorem Theorem 4.1 (Value -Independence Implies Constant Marginal; Universal). Let 𝑞 > 0. Let 𝛽 be any type with decidable equality. Let 𝑤: ℤ𝑞 × ℤ𝑞 → 𝛽 be a wire function. Define the marginal histogram ℎ(𝑥, 𝑣) : = |{𝑠1 ∈ ℤ𝑞: 𝑤(𝑥 − 𝑠1, 𝑠1) = 𝑣}|. If 𝑤 is value-independent (Definition 3), then for all 𝑥, 𝑥′ ∈ ℤ𝑞 and all 𝑣 ∈ 𝛽: ℎ(𝑥, 𝑣) = ℎ(𝑥′, 𝑣). ...

    work page

  15. [15]

    The marginal histogram counts elements of a filtered finite set: those 𝑠1 ∈ ℤ𝑞 for which 𝑤(𝑥 − 𝑠1, 𝑠1) = 𝑣

    Unfold the definition. The marginal histogram counts elements of a filtered finite set: those 𝑠1 ∈ ℤ𝑞 for which 𝑤(𝑥 − 𝑠1, 𝑠1) = 𝑣

    work page

  16. [16]

    Two finite sets with the same elements have the same cardinality (congr 1 reduces the cardinality goal to a set-extensionality goal)

    Reduce to set equality. Two finite sets with the same elements have the same cardinality (congr 1 reduces the cardinality goal to a set-extensionality goal)

    work page

  17. [17]

    For each 𝑠1, the filter predicate 𝑤(𝑥 − 𝑠1, 𝑠1) = 𝑣 holds if and only if 𝑤(𝑥′ − 𝑠1, 𝑠1) = 𝑣

    Pointwise equivalence. For each 𝑠1, the filter predicate 𝑤(𝑥 − 𝑠1, 𝑠1) = 𝑣 holds if and only if 𝑤(𝑥′ − 𝑠1, 𝑠1) = 𝑣. This is immediate from value -independence: 𝑤(𝑥 − 𝑠1, 𝑠1) = 𝑤(𝑥′ − 𝑠1, 𝑠1)

    work page

  18. [18]

    The two directions of the biconditional each follow by a single rewrite using the value-independence hypothesis

    Close the iff. The two directions of the biconditional each follow by a single rewrite using the value-independence hypothesis. The Z3/CVC5 proof at 𝑞 = 5 required checking 225 = 33,554,432 Boolean wire functions because SMT solvers must instantiate universal quantifiers. Lean 4’s dependent type theory handles the universal quantification natively: the pr...

    work page

  19. [19]

    All nine theorems are sorry - free

    The Supporting Proof Suite Figure 1 shows the logical dependencies among the theorems. All nine theorems are sorry - free. T1, T1’, T2, T3, T3’, T4, T5 universal bounds, and T6 are kernel -verified. T5’s ML - KEM instance is verified by native compilation ( native_decide); see Section 5.4. Table 2 summarizes each theorem’s scope, key proof technique, and ...

    work page

  20. [20]

    Constant marginal. For any 𝑥, 𝑥′, the sets {𝑠1: (𝑥 − 𝑠1) = 0} and {𝑠1: (𝑥′ − 𝑠1) = 0} have the same cardinality because the translation map 𝑠1 ↦ 𝑠1 + (𝑥′ − 𝑥) is a bijection between them (Finset.card_bij)

    work page

  21. [21]

    We have 𝑤(0 − 0,0) = [0 = 0] = true but 𝑤(1 − 0,0) = [1 = 0], which is false because 1 ≠ 0 in ℤ𝑞 when 𝑞 ≥ 2

    Not value-independent. We have 𝑤(0 − 0,0) = [0 = 0] = true but 𝑤(1 − 0,0) = [1 = 0], which is false because 1 ≠ 0 in ℤ𝑞 when 𝑞 ≥ 2. The non -triviality of ℤ𝑞 is established by Mathlib’s one_ne_zero, which requires only 𝑞 ≥ 2. The Lean 4 formalization of this counterexample follows: theorem converse_fails_universal {q : ℕ} [NeZero q] (hq : 2 ≤ q) : ∃ (w : ...

    work page

  22. [22]

    trust Z3 and CVC5 on 225 instances

    Implications 6.1. For FIPS 140-3 Certification FIPS 140-3 [22] certification of cryptographic modules requires evidence that side -channel countermeasures are effective. A universal proof eliminates the need to re -verify for each parameter set: a single kernel -verified proof covers ML -KEM ( 𝑞 = 3,329), ML-DSA ( 𝑞 = 8,380,417), and any future NIST PQC s...

    work page

  23. [23]

    Paper 4 will close this gap

    Limitations and Future Work The two primary limitations below are related: together they constitute the single remaining gap between the formalized result (constant marginal histogram) and a complete machine - checked proof of 𝐼(𝑥; 𝑤) = 0 under fresh randomness. Paper 4 will close this gap. (i) 𝑟-free sub-theorem. T1 proves the 𝑟-free version of Theorem 3...

    work page

  24. [24]

    Conclusion We have presented, to our knowledge, the first machine -checked universal proof that value - independence implies distributional security ( 𝑟-free sub-theorem) for arithmetic masking in NTT-based PQC hardware. The proof, mechanized in Lean 4 with Mathlib, closes the finite - domain gap explicitly identified in the QANARY framework: a soundness ...

    work page

  25. [25]

    Code and Data Availability The complete Lean 4 proof suite supporting this paper is publicly available at https://github.com/rayiskander2406/qanary-universal-masking-proofs-arXiv-2604.18717 under the MIT license, with an archival snapshot of version v1.0.0 deposited on Zenodo at https://doi.org/10.5281/zenodo.19689480. The repository contains the complete...

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

  26. [26]

    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. Archived at https://doi.org/10.5281/zenodo.19625392. (Paper 1 in this series.)

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

  27. [27]

    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. Archived at https://doi.org/10.5281/zenodo.19508454. (Paper 2 in this series.)

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

  28. [28]

    Adams Bridge Accelerator: Bridging the Post-Quantum Transition,

    M. Bisheh-Niasar, E. Karabulut, B. Upadhyayula, A. Norris, and L. Pillilli, “Adams Bridge Accelerator: Bridging the Post-Quantum Transition,” IACR ePrint 2026/256, 2026

    work page 2026

  29. [29]

    Adams Bridge: Open-Source Post-Quantum Cryptographic Accelerator,

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

    work page 2024

  30. [30]

    Module-Lattice-Based Key- Encapsulation Mechanism Standard,

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

    work page 2024

  31. [31]

    Module-Lattice-Based Digital Signature Standard,

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

    work page 2024

  32. [32]

    Transition to Post-Quantum Cryptography Standards,

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

    work page 2025

  33. [33]

    The Lean 4 Theorem Prover and Programming Language,

    L. de Moura and S. Ullrich, “The Lean 4 Theorem Prover and Programming Language,” https://lean-lang.org, 2021

    work page 2021

  34. [34]

    Mathlib4: The Math Library for Lean 4,

    Mathlib Community, “Mathlib4: The Math Library for Lean 4,” https://github.com/leanprover-community/mathlib4, 2024

    work page 2024

  35. [35]

    Z3: An Efficient SMT Solver,

    L. de Moura and N. Bjorner, “Z3: An Efficient SMT Solver,” in TACAS, 2008

    work page 2008

  36. [36]

    cvc5: A Versatile and Industrial-Strength SMT Solver,

    H. Barbosa et al., “cvc5: A Versatile and Industrial-Strength SMT Solver,” in TACAS, 2022

    work page 2022

  37. [37]

    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,” IEEE HOST, 2025. IACR ePrint 2025/009

    work page 2025

  38. [38]

    Private Circuits: Securing Hardware against Probing Attacks,

    Y. Ishai, A. Sahai, and D. Wagner, “Private Circuits: Securing Hardware against Probing Attacks,” in CRYPTO, 2003

    work page 2003

  39. [39]

    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,” in EUROCRYPT, 2015

    work page 2015

  40. [40]

    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,” in EUROCRYPT, 2018. Iskander & Kirah — Ring-Theoretic Foundations for PQC Masking Verification 15

    work page 2018

  41. [41]

    SILVER – Statistical Independence and Leakage Verification,

    D. Knichel, P. Sasdrich, and A. Moradi, “SILVER – Statistical Independence and Leakage Verification,” in ASIACRYPT, 2020

    work page 2020

  42. [42]

    Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs,

    B. Gigerl, V. Hadzic, R. Primas, S. Mangard, and R. Bloem, “Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs,” in USENIX Security, 2021

    work page 2021

  43. [43]

    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 ACNS, 2023

    work page 2023

  44. [44]

    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,” in ACM CCS, 2016

    work page 2016

  45. [45]

    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 ACM TIS, 2016

    work page 2016

  46. [46]

    A Sound Method for Switching between Boolean and Arithmetic Masking,

    L. Goubin, “A Sound Method for Switching between Boolean and Arithmetic Masking,” in CHES, 2001

    work page 2001

  47. [47]

    Security Requirements for Cryptographic Modules,

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

    work page 2019