pith. sign in

arxiv: 2605.23316 · v2 · 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.