pith. sign in

arxiv: 2605.23316 · v1 · pith:NX4SR2DMnew · submitted 2026-05-22 · 💻 cs.LO · cs.CR

Formal Verification of Probing Security via Conditional Independence

Satoshi Kura , Katsuyuki Takashima This is my paper

Pith reviewed 2026-05-25 03:19 UTC · model grok-4.3

classification 💻 cs.LO cs.CR
keywords formal verificationprobing securitymasking countermeasuresconditional independenceseparation logicnoninterferenceside-channel attacksLilac logic
0
0 comments X

The pith

Noninterference properties of masked algorithms can be verified by reducing them to conditional independence in Lilac separation logic.

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

The paper connects noninterference, a security property for masked cryptographic algorithms, directly to conditional independence. This link lets existing proof systems for conditional independence handle verification of probing security. Several new proof rules are supplied to make the checks practical on concrete masked algorithms. A reader would care because manual security arguments for masking are error-prone and side-channel attacks remain a practical threat.

Core claim

Noninterference of masked algorithms is equivalent to a form of conditional independence, so the Lilac separation logic for conditional independence can be used to verify probing security, supported by additional proof rules that the authors introduce and apply to example algorithms.

What carries the argument

Lilac, the separation logic for conditional independence, linked to noninterference through an explicit correspondence plus several new proof rules that simplify verification of probing security.

If this is right

  • Probing security checks for masked code can reuse any existing Lilac proofs or tools developed for conditional independence.
  • The supplied proof rules reduce the manual effort needed to establish noninterference for typical masking schemes.
  • Verification becomes compositional because separation logic naturally handles independent components of a masked circuit.
  • The method applies directly to the example algorithms shown in the paper, confirming it scales at least to small masked implementations.

Where Pith is reading between the lines

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

  • The same correspondence could extend verification to other leakage models beyond probing if conditional independence can be restated for those models.
  • Integration with existing program logics for cryptographic code would allow end-to-end security arguments that include both functional correctness and side-channel resistance.
  • Automated tactics for the new rules could turn the approach into a practical tool rather than a manual proof exercise.

Load-bearing premise

The Lilac logic plus the new proof rules accurately capture the probabilistic noninterference semantics of masked algorithms without missing side conditions.

What would settle it

A masked algorithm that is noninterfering by the standard probabilistic definition but cannot be proved secure in Lilac, or an algorithm that is proved secure in Lilac yet leaks information under probing.

Figures

Figures reproduced from arXiv: 2605.23316 by Katsuyuki Takashima, Satoshi Kura.

Figure 1
Figure 1. Figure 1: Two formulations of security: simulator-based formulation and conditional-independence-based formulation. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Typing rule for APPL programs. O = {Y1, . . . , Yn} for the set of output variables of M. For I ⊆ I and O ⊆ O, we say that M is (I, O)-noninterfering ((I, O)-NI) if there exists an APPL program ∆I ⊢ Sim(M) : GBO such that the following equation holds: Sim(M) = O ← M; ret O Q Here, ∆I is the restriction of ∆ to variables in I and BO = Yi∈O Bi is the restriction of B to components in O. We call such a progra… view at source ↗
Figure 3
Figure 3. Figure 3: Selected inference rules for Lilac formulas [29]. See Fig. 12 in the appendix for a more comprehensive list of rules. [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Inference rules for Hoare triples in Lilac [29] [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: AddRepNoiseER [32] in conventional pseudocode. [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: MiniAddRepNoise in conventional pseudocode. [PITH_FULL_IMAGE:figures/full_fig_p010_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: This algorithm takes a shared input V = (V 0 , . . . , V t ) and an unshared input ρ = (ρ0, . . . , ρt). The output is X = (X0 , . . . , Xt ), and there are no internal variables. Theorem VII.1. Let O ⊆ X be a set of probed variables such that |O| ≤ t. We define I = I shared MARN(O) ∪ Iunshared MARN (O) by I shared MARN(O) := {V j | Xj ∈ O} and I unshared MARN (O) := [PITH_FULL_IMAGE:figures/full_fig_p010… view at source ↗
Figure 8
Figure 8. Figure 8: Algorithm REFRESH [9] in conventional pseudocode. Subscripts for C are used to conform to single-assignment style but may be omitted if multiple assignments to C are allowed. Since Xj as= v j + rj is deterministic, we have □ own Xj for each Xj ∈ O. Thus, we obtain the desired postcondition. Details of the proof are given in Appendix D-A. Remark VII.2. As explained in Section III-B, reasoning about noninter… view at source ↗
Figure 7
Figure 7. Figure 7: Algorithm MINIADDREPNOISE in APPL. Gray lines show the proof outline for Theorem VII.1. We apply the H￾FOR rule to the loop with the loop invariant I(j; X). {ρj | Xj ∈ O} (here, “MARN” stands for MiniAddRepNoise). Then, the following Hoare triple is derivable in Lilac, meaning that MINIADDREPNOISE is (I, O)-NI. {own(V, ρ)} for (X ← 0; j ← 0, . . . , t) { ret X[V j + ρj/Xj ] } { C (v,r)←(V∩I,ρ∩I) (own(V \ I… view at source ↗
Figure 9
Figure 9. Figure 9: Algorithm REFRESH in APPL. Here, R is a shorthand for the collection of random variables Ri,j , and C = (C0, . . . , Ct) where Ci = (C 0 i , . . . , Ct i ) for each i. Gray comments show the proof outline for Theorem VII.4. In the invariant, <lex denotes the lexicographic order on pairs of integers (i, j) such that i < j, and f i j (R) is a function defined in (6). We can derive the desired postcondition b… view at source ↗
Figure 10
Figure 10. Figure 10: Algorithm SECMULT in conventional pseudocode. Unlike the presentation in [9], our version computes Pi,j ← Ai × Bj for all i, j in advance, since we need to assign a distinct variable name to each Ai × Bj for the proof. ( Pt i=0 Ai ) × ( Pt i=0 Bi ). It is proved in [9] that SECMULT is t-SNI. We show that by Theorem V.1, this result can be proved in Lilac as well. Theorem VII.8. Let O be a set of probed va… view at source ↗
Figure 11
Figure 11. Figure 11: Algorithm SECMULT in APPL. Here, Q, R, and S are shorthands for the collection of random variables {Qi,j | 0 ≤ i < j ≤ t}, {Ri,j | 0 ≤ i < j ≤ t}, and {Si,j | 0 ≤ i < j ≤ t}, respectively; and C = (C0, . . . , Ct) where Ci = (C 0 i , . . . , Ct i ) for each i. Gray comments show the proof outline for Theorem VII.8, but we omit some straightforward proof steps for brevity. The function g i j (Q, S) is defi… view at source ↗
Figure 12
Figure 12. Figure 12: List of inference rules for Lilac formulas [29]. We omit obvious structural rules like commutativity and associativity [PITH_FULL_IMAGE:figures/full_fig_p024_12.png] view at source ↗
read the original abstract

Side-channel attacks are a major threat to the security of cryptosystems. Masking is a widely used countermeasure against such attacks, but proving the security of masked algorithms is error-prone without formal verification. In this work, we propose a novel approach to formal verification of noninterference properties of masked algorithms based on probabilistic separation logic. By establishing a connection between noninterference and conditional independence, we show how noninterference can be verified using Lilac, a separation logic for conditional independence. We also provide several proof rules that facilitate the verification of probing security and demonstrate their application to example algorithms.

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 / 0 minor

Summary. The paper claims that noninterference properties of masked algorithms (for probing security against side-channel attacks) can be verified by establishing a connection to conditional independence and using the existing Lilac separation logic, augmented with several new proof rules whose application is demonstrated on example algorithms.

Significance. If the embedding of noninterference into Lilac is shown to be sound and the new rules are proven correct with respect to the probabilistic semantics of masked circuits, the work would supply a reusable formal tool for a practically important verification task in cryptography.

major comments (1)
  1. [Abstract] The central claim rests on the unexamined assumption that Lilac's conditional-independence rules plus the new proof rules correctly capture the probabilistic noninterference semantics without introducing unsoundness or requiring additional side conditions on mask distributions; no soundness argument, semantic embedding, or example derivation is available for inspection.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review. We address the major comment on the soundness of the embedding below.

read point-by-point responses

  1. Referee: [Abstract] The central claim rests on the unexamined assumption that Lilac's conditional-independence rules plus the new proof rules correctly capture the probabilistic noninterference semantics without introducing unsoundness or requiring additional side conditions on mask distributions; no soundness argument, semantic embedding, or example derivation is available for inspection.

    Authors: The abstract is necessarily concise. The full manuscript examines the assumption in detail: Section 2 recalls the probabilistic semantics of masked circuits and defines noninterference; Section 3 proves the equivalence between noninterference and conditional independence (under the standard uniform independent mask distribution) and shows that this equivalence licenses direct application of Lilac's rules; Section 4 introduces the new probing-specific rules and proves them sound with respect to the same semantics, with no extra side conditions required. Concrete derivations appear in Section 6. We can add an explicit reference to these sections in a revised abstract if the editor prefers. revision: no

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper establishes a semantic connection between noninterference and conditional independence, then uses the existing Lilac logic plus new proof rules to verify probing security on masked algorithms. No equations, definitions, or claims in the provided abstract reduce a derived result to a fitted parameter, self-citation chain, or renamed input by construction. The central claim (connection + rules) retains independent content outside any self-referential loop.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on the soundness of the existing Lilac logic (standard in separation-logic literature) and on the claim that the new proof rules preserve that soundness for the specific noninterference property; no free parameters or invented entities are visible from the abstract.

axioms (1)
  • standard math Lilac separation logic is sound for reasoning about conditional independence in probabilistic programs.
    Invoked implicitly when the paper states that noninterference can be verified using Lilac.

pith-pipeline@v0.9.0 · 5618 in / 1159 out tokens · 28714 ms · 2026-05-25T03:19:24.703547+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

51 extracted references · 28 canonical work pages

  1. [1]

    Private Circuits: Securing Hardware against Probing Attacks,

    Y . Ishai, A. Sahai, and D. Wagner, “Private Circuits: Securing Hardware against Probing Attacks,” inAdvances in Cryptology - CRYPTO 2003, ser. Lecture Notes in Computer Science, vol. 2729. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003, pp. 463–481. [Online]. Available: http://link.springer.com/10.1007/978-3-540-45146-4 27

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

  2. [2]

    Raccoon,

    R. Del Pino, T. Espitau, S. Katsumata, M. Maller, F. Mouhartem, T. Prest, M. Rossi, and M.-J. Saarinen, “Raccoon,” National Institute of Standards and Technology, Technical Report, 2023. [Online]. Available: https://csrc.nist.gov/Projects/pqc-dig-sig/round-1-additional-signatures

    2023

  3. [3]

    Improved Gadgets for the High-Order Masking of Dilithium,

    J.-S. Coron, F. G ´erard, M. Trannoy, and R. Zeitoun, “Improved Gadgets for the High-Order Masking of Dilithium,”IACR Transactions on Cryptographic Hardware and Embedded Systems, vol. 2023, no. 4, pp. 110–145, Aug. 2023. [Online]. Available: https://tches.iacr.org/index. php/TCHES/article/view/11160

    2023

  4. [4]

    Improved High-Order Masked Generation of Masking Vector and Rejection Sampling in Dilithium,

    J.-S. Coron, F. G ´erard, T. Lepoint, M. Trannoy, and R. Zeitoun, “Improved High-Order Masked Generation of Masking Vector and Rejection Sampling in Dilithium,”IACR Transactions on Cryptographic Hardware and Embedded Systems, vol. 2024, no. 4, pp. 335–354, Sep. 2024. [Online]. Available: https://tches.iacr.org/index.php/TCHES/ article/view/11795

    2024

  5. [5]

    Finding and Protecting the Weakest Link - On Side-Channel Attacks on y in Masked ML-DSA,

    J. Hermelink, K.-C. Ning, and R. Petri, “Finding and Protecting the Weakest Link - On Side-Channel Attacks on y in Masked ML-DSA,” in Advances in Cryptology – CRYPTO 2025, (to appear), 2025, pp. xx–xx

    2025

  6. [6]

    Module-lattice- based digital signature standard,

    National Institute of Standards and Technology (US), “Module-lattice- based digital signature standard,” National Institute of Standards and Technology (U.S.), Washington, D.C., Tech. Rep. NIST FIPS 204, Aug. 2024. [Online]. Available: https://nvlpubs.nist.gov/nistpubs/FIPS/ NIST.FIPS.204.pdf

    2024

  7. [7]

    A Key-Recovery Attack Against Mitaka in the t- Probing Model,

    T. Prest, “A Key-Recovery Attack Against Mitaka in the t- Probing Model,” inPublic-Key Cryptography – PKC 2023, ser. Lecture Notes in Computer Science, vol. 13940. Cham: Springer Nature Switzerland, 2023, pp. 205–220. [Online]. Available: https: //link.springer.com/10.1007/978-3-031-31368-4 8

    work page doi:10.1007/978-3-031-31368-4 2023

  8. [8]

    Higher-Order Side Channel Security and Mask Refreshing,

    J.-S. Coron, E. Prouff, M. Rivain, and T. Roche, “Higher-Order Side Channel Security and Mask Refreshing,” inFast Software Encryption, ser. Lecture Notes in Computer Science, vol. 8424. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, pp. 410–424. [Online]. Available: https://link.springer.com/10.1007/978-3-662-43933-3 21

    work page doi:10.1007/978-3-662-43933-3 2014

  9. [9]

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

    G. Barthe, S. Bela ¨ıd, F. Dupressoir, P.-A. Fouque, B. Gr ´egoire, P.-Y . Strub, and R. Zucchini, “Strong Non-Interference and Type- Directed Higher-Order Masking,” inProceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. Vienna Austria: ACM, Oct. 2016, pp. 116–129. [Online]. Available: https://dl.acm.org/doi/10.1145/29767...

    work page doi:10.1145/2976749.2978427 2016

  10. [10]

    Verified Proofs of Higher-Order Masking,

    G. Barthe, S. Bela ¨ıd, F. Dupressoir, P.-A. Fouque, B. Gr ´egoire, and P.-Y . Strub, “Verified Proofs of Higher-Order Masking,” in Advances in Cryptology – EUROCRYPT 2015, ser. Lecture Notes in Computer Science, vol. 9056. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015, pp. 457–485. [Online]. Available: http: //link.springer.com/10.1007/978-3-662-4...

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

  11. [11]

    maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults,

    G. Barthe, S. Bela ¨ıd, G. Cassiers, P.-A. Fouque, B. Gr ´egoire, and F.-X. Standaert, “maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults,” inComputer Security – ESORICS 2019, ser. Lecture Notes in Computer Science, vol. 11735. Cham: Springer International Publishing, 2019, pp. 300–318. [Online]. Available: https:/...

    work page doi:10.1007/978-3-030-29959-0 2019

  12. [12]

    SCInfer: Refinement- Based Verification of Software Countermeasures Against Side- Channel Attacks,

    J. Zhang, P. Gao, F. Song, and C. Wang, “SCInfer: Refinement- Based Verification of Software Countermeasures Against Side- Channel Attacks,” inComputer Aided Verification, ser. Lecture Notes in Computer Science, vol. 10982. Cham: Springer International Publishing, 2018, pp. 157–177. [Online]. Available: http://link.springer. com/10.1007/978-3-319-96142-2 12

    work page doi:10.1007/978-3-319-96142-2 2018

  13. [13]

    A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs,

    P. Gao, H. Xie, F. Song, and T. Chen, “A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs,” ACM Transactions on Software Engineering and Methodology, vol. 30, no. 3, pp. 1–42, Jul. 2021. [Online]. Available: https: //dl.acm.org/doi/10.1145/3428015

    work page doi:10.1145/3428015 2021

  14. [14]

    Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks,

    P. Gao, H. Xie, J. Zhang, F. Song, and T. Chen, “Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks,” inTools and Algorithms for the Construction and Analysis of Systems, ser. Lecture Notes in Computer Science, vol. 11427. Cham: Springer International Publishing, 2019, pp. 155–173. [Online]. Available: http://link.springe...

    work page doi:10.1007/978-3-030-17462-0 2019

  15. [15]

    Compositional Verification of First- Order Masking Countermeasures against Power Side-Channel Attacks,

    P. Gao, F. Song, and T. Chen, “Compositional Verification of First- Order Masking Countermeasures against Power Side-Channel Attacks,” ACM Transactions on Software Engineering and Methodology, vol. 33, no. 3, pp. 1–38, Mar. 2024. [Online]. Available: https: //dl.acm.org/doi/10.1145/3635707

    work page doi:10.1145/3635707 2024

  16. [16]

    Formal Verification of Software Countermeasures against Side-Channel Attacks,

    H. Eldib, C. Wang, and P. Schaumont, “Formal Verification of Software Countermeasures against Side-Channel Attacks,”ACM Transactions on Software Engineering and Methodology, vol. 24, no. 2, pp. 1–24, Dec

  17. [17]

    Available: https://dl.acm.org/doi/10.1145/2685616

    [Online]. Available: https://dl.acm.org/doi/10.1145/2685616

    work page doi:10.1145/2685616

  18. [18]

    Formal Verification of Side-Channel Countermeasures via Elementary Circuit Transformations,

    J.-S. Coron, “Formal Verification of Side-Channel Countermeasures via Elementary Circuit Transformations,” inApplied Cryptography and Network Security, ser. Lecture Notes in Computer Science, vol. 10892. Cham: Springer International Publishing, 2018, pp. 65–82. [Online]. Available: https://link.springer.com/10.1007/978-3-319-93387-0 4

    work page doi:10.1007/978-3-319-93387-0 2018

  19. [20]

    SILVER – Statistical Independence and Leakage Verification,

    D. Knichel, P. Sasdrich, and A. Moradi, “SILVER – Statistical Independence and Leakage Verification,” inAdvances in Cryptology – ASIACRYPT 2020, ser. Lecture Notes in Computer Science, vol. 12491. Cham: Springer International Publishing, 2020, pp. 787–816. [Online]. Available: https://link.springer.com/10.1007/978-3-030-64837-4 26

    work page doi:10.1007/978-3-030-64837-4 2020

  20. [21]

    LeakageVerif: Efficient and Scalable Formal Verification of Leakage in Symbolic Expressions,

    Q. L. Meunier, E. Pons, and K. Heydemann, “LeakageVerif: Efficient and Scalable Formal Verification of Leakage in Symbolic Expressions,”IEEE Transactions on Software Engineering, vol. 49, no. 6, pp. 3359–3375, Jun. 2023. [Online]. Available: https: //ieeexplore.ieee.org/document/10059223/

    work page arXiv 2023

  21. [22]

    A probabilistic separation logic,

    G. Barthe, J. Hsu, and K. Liao, “A probabilistic separation logic,”Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, pp. 1–30, Jan. 2020. [Online]. Available: https://dl.acm.org/doi/10.1145/3371123

    work page doi:10.1145/3371123 2020

  22. [23]

    Separation logic: A logic for shared mutable data structures,

    J. Reynolds, “Separation logic: A logic for shared mutable data structures,” inProceedings 17th Annual IEEE Symposium on Logic in Computer Science. Copenhagen, Denmark: IEEE Computer Society, 2002, pp. 55–74. [Online]. Available: http://ieeexplore.ieee.org/ document/1029817/

    work page arXiv 2002

  23. [24]

    A Bunched Logic for Conditional Independence,

    J. Bao, S. Docherty, J. Hsu, and A. Silva, “A Bunched Logic for Conditional Independence,” in2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Rome, Italy: IEEE, Jun. 2021, pp. 1–14. [Online]. Available: https://ieeexplore.ieee.org/ document/9470712/

    work page arXiv 2021

  24. [25]

    Bayesian Separation Logic: A Logical Foundation and Axiomatic Semantics for Probabilistic Programming,

    S. H. Ho, N. Wu, and A. Raad, “Bayesian Separation Logic: A Logical Foundation and Axiomatic Semantics for Probabilistic Programming,”Proceedings of the ACM on Programming Languages, vol. 10, no. POPL, pp. 1557–1585, Jan. 2026. [Online]. Available: https://dl.acm.org/doi/10.1145/3776696

    work page doi:10.1145/3776696 2026

  25. [26]

    Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning,

    J. Bao, E. D’Osualdo, and A. Farzan, “Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning,” Proceedings of the ACM on Programming Languages, vol. 9, no. POPL, pp. 1719–1749, Jan. 2025. [Online]. Available: https: //dl.acm.org/doi/10.1145/3704894

    work page doi:10.1145/3704894 2025

  26. [27]

    Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants,

    N. Zilberstein, A. Silva, and J. Tassarotti, “Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants,”Proceedings of the ACM on Programming Languages, vol. 10, no. POPL, pp. 235–264, Jan. 2026. [Online]. Available: https://dl.acm.org/doi/10.1145/3776651

    work page doi:10.1145/3776651 2026

  27. [28]

    On Separation Logic, Computational Independence, and Pseudorandomness,

    U. Dal Lago, D. Davoli, and B. M. Kapron, “On Separation Logic, Computational Independence, and Pseudorandomness,” in2024 IEEE 37th Computer Security Foundations Symposium (CSF). Enschede, Netherlands: IEEE, Jul. 2024, pp. 80–95. [Online]. Available: https://ieeexplore.ieee.org/document/10664346/

    work page arXiv 2024

  28. [29]

    A separation logic for negative dependence,

    J. Bao, M. Gaboardi, J. Hsu, and J. Tassarotti, “A separation logic for negative dependence,”Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, pp. 1–29, Jan. 2022. [Online]. Available: https://dl.acm.org/doi/10.1145/3498719

    work page doi:10.1145/3498719 2022

  29. [30]

    Lilac: A Modal Separation Logic for Conditional Probability,

    J. M. Li, A. Ahmed, and S. Holtzen, “Lilac: A Modal Separation Logic for Conditional Probability,”Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, pp. 148–171, Jun. 2023. [Online]. Available: https://dl.acm.org/doi/10.1145/3591226

    work page doi:10.1145/3591226 2023

  30. [31]

    A Nominal Approach to Probabilistic Separation Logic,

    J. M. Li, J. Aytac, P. Johnson-Freyd, A. Ahmed, and S. Holtzen, “A Nominal Approach to Probabilistic Separation Logic,” inProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science. Tallinn Estonia: ACM, Jul. 2024, pp. 1–14. [Online]. Available: https://dl.acm.org/doi/10.1145/3661814.3662135

    work page doi:10.1145/3661814.3662135 2024

  31. [32]

    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. [Online]. Available: https://ieeexplore.ieee.org/document/ 8979162/

    2020

  32. [33]

    Raccoon: A Masking-Friendly Signature Proven in the Probing Model,

    R. Del Pino, S. Katsumata, T. Prest, and M. Rossi, “Raccoon: A Masking-Friendly Signature Proven in the Probing Model,” in Advances in Cryptology – CRYPTO 2024, ser. Lecture Notes in Computer Science, vol. 14920. Cham: Springer Nature Switzerland, 2024, pp. 409–444. [Online]. Available: https://link.springer.com/10. 1007/978-3-031-68376-3 13

    2024

  33. [34]

    Communication Theory of Secrecy Systems,

    C. E. Shannon, “Communication Theory of Secrecy Systems,”Bell System Technical Journal, vol. 28, no. 4, pp. 656–715, Oct. 1949. [Online]. Available: https://ieeexplore.ieee.org/document/6769090

    work page arXiv 1949

  34. [35]

    plover: Masking-friendly hash-and-sign lattice signatures,

    M. F. Esgin, T. Espitau, G. Niot, T. Prest, A. Sakzad, and R. Steinfeld, “plover: Masking-friendly hash-and-sign lattice signatures,” inAdvances in Cryptology – EUROCRYPT 2024, ser. Lecture Notes in Computer Science, vol. 14657. Cham: Springer Nature Switzerland, 2024, pp. 316–345. [Online]. Available: https://link.springer.com/10.1007/ 978-3-031-58754-2 12

    2024

  35. [36]

    Masking the GLP Lattice-Based Signature Scheme at Any Order,

    G. Barthe, S. Bela ¨ıd, T. Espitau, P.-A. Fouque, B. Gr ´egoire, M. Rossi, and M. Tibouchi, “Masking the GLP Lattice-Based Signature Scheme at Any Order,” inAdvances in Cryptology – EUROCRYPT 2018, ser. Lecture Notes in Computer Science, vol. 10821. Cham: Springer International Publishing, 2018, pp. 354–384. [Online]. Available: https://link.springer.com/...

    work page doi:10.1007/978-3-319-78375-8 2018

  36. [37]

    Iris from the ground up: A modular foundation for higher- order concurrent separation logic,

    R. Jung, R. Krebbers, J.-H. Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer, “Iris from the ground up: A modular foundation for higher- order concurrent separation logic,”Journal of Functional Programming, vol. 28, p. e20, 2018. [Online]. Available: https://www.cambridge.org/ core/product/identifier/S0956796818000151/type/journal article

    2018

  37. [38]

    The semantics of BI and resource tableaux,

    D. Galmiche, D. M ´ery, and D. Pym, “The semantics of BI and resource tableaux,”Mathematical Structures in Computer Science, vol. 15, no. 6, pp. 1033–1088, Dec. 2005. [Online]. Available: https://www.cambridge. org/core/product/identifier/S0960129505004858/type/journal article

    2005

  38. [39]

    Conditioning as disintegration,

    J. T. Chang and D. Pollard, “Conditioning as disintegration,”Statistica Neerlandica, vol. 51, no. 3, pp. 287–317, Nov. 1997. [Online]. Available: https://onlinelibrary.wiley.com/doi/abs/10.1111/1467-9574.00056

    work page doi:10.1111/1467-9574.00056 1997

  39. [40]

    Graphoids: Graph-Based Logic for Reasoning about Relevance Relations or When would x tell you more about y if you already know z?

    J. Pearl and A. Paz, “Graphoids: Graph-Based Logic for Reasoning about Relevance Relations or When would x tell you more about y if you already know z?” inAdvances in Artificial Intelligence II, Seventh European Conference on Artificial Intelligence, ECAI 1986, Brighton, UK, July 20-25. North-Holland, 1986, pp. 357–363

    1986

  40. [41]

    A semantics for concurrent separation logic,

    S. Brookes, “A semantics for concurrent separation logic,” Theoretical Computer Science, vol. 375, no. 1-3, pp. 227–270, May 2007. [Online]. Available: https://linkinghub.elsevier.com/retrieve/ pii/S0304397506009248

    2007

  41. [42]

    Symbolic approach for side-channel resistance analysis of masked assembly codes,

    I. B. E. Ouahma, Q. Meunier, K. Heydemann, and E. Encrenaz, “Symbolic approach for side-channel resistance analysis of masked assembly codes,” inPROOFS 2017. 6th International Workshop on Security Proofs for Embedded Systems, ser. EPiC Series in Computing, vol. 49. EasyChair, 2017, pp. 17–32. [Online]. Available: /publications/paper/9Bpn

    2017

  42. [43]

    Side-channel robustness analysis of masked assembly codes using a symbolic approach,

    I. Ben El Ouahma, Q. L. Meunier, K. Heydemann, and E. Encrenaz, “Side-channel robustness analysis of masked assembly codes using a symbolic approach,”Journal of Cryptographic Engineering, vol. 9, no. 3, pp. 231–242, Sep. 2019. [Online]. Available: http://link.springer. com/10.1007/s13389-019-00205-7 A BASICFACTS ABOUTPROBABILITYTHEORY Letf:A→Bbe a measura...

    work page doi:10.1007/s13389-019-00205-7 2019

  43. [44]

    Therefore, we have JM ′K(a1, a2) =JM ′K(a1, a′ 2), which is a contradiction

    By Lemma B.6, we have(Y 1)∗νx1,x2 =JMK(x 1, x2)for almost all(x 1, x2), i.e., for any(x 1, x2)∈ {(a 1, a2),(a 1, a′ 2)}. Therefore, we have JM ′K(a1, a2) =JM ′K(a1, a′ 2), which is a contradiction. For the (⇐=) direction of Theorem V .1, the key lemma is the following. Lemma B.10.Let∆ =X 1 :A 1, . . . , Xn :A n be a context,∆⊢M:GBbe an APPL program, andZ∈...

  44. [45]

    IfC i j ∈ Oandj < t, theni∈I∩J

  45. [46]

    Ifi < j,C i j ∈ O, andi < k≤j < t, then(i, k)∈K Q

  46. [47]

    IfC i j ∈ O,k < i,j < t, and(k, i)∈K Q, thenk, i∈Iandk, i∈J

  47. [48]

    IfQ i,j ∈ O, then(i, j)∈K Q

  48. [49]

    IfR i,j ∈ O, then(i, j)∈K Q,i∈I, andj∈J

  49. [50]

    If(i, j)∈K Q andS i,j ∈ O, theni, j∈Iandi, j∈J

  50. [51]

    IfC i t ∈ Oand there existsj < twithC i j ∈ O, thenV i ⊆K Q ∪K S

  51. [52]

    Here,V i ={(k, i)|k < i} ∪ {(i, k)|i < k}is the indices of the free variables ing i t(Q,S)

    IfC i t ∈ Oand there is noj < twithC i j ∈ O, thenV i \(K Q ∪K S)̸=∅. Here,V i ={(k, i)|k < i} ∪ {(i, k)|i < k}is the indices of the free variables ing i t(Q,S). Condition 9 follows because |Vi ∩(K Q ∪K S)| ≤ |O \C t|<|V i|=t. Vi ∩(K Q ∪K S) =V i ∩ {(i, j)|Q i,j ∈Q∨R i,j ∈ O ∨S i,j ∈ O} ∪ {(k, i)|k < i, C k j ∈ O, j < t} ∪ {(i, k)|i < k, C k j ∈ O, j < t}...