Formal Verification of Probing Security via Conditional Independence

Unknown

Conceptio › Archive › arXiv CS

arXiv CSopen access

Formal Verification of Probing Security via Conditional Independence

Unknown · 2026 · arxiv_cs

arXiv CS · Papers · License: Open Access · 2026

Open Source ↗Direct PDF ↓

cryptography cybersecurity privacy security

cryptography, security, privacy, cybersecurity

arXiv:2605.23316v1 [cs.LO] 22 May 2026

Formal Verification of Probing Security via Conditional Independence Satoshi Kura

Katsuyuki Takashima

Faculty of Education and Integrated Arts and Sciences Waseda University Tokyo, Japan ORCID: 0000-0002-3954-8255

Faculty of Education and Integrated Arts and Sciences Waseda University Tokyo, Japan ORCID: 0000-0001-5216-2229

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. Index Terms—Side-channel attack, Masking, Noninterference, Conditional independence, Formal verification, Probabilistic separation logic

I. I NTRODUCTION A. Formal Verification of Probing Security Information leakage through side-channel attacks is one of the major threats to the security of cryptographic schemes and digital signatures. Among the widely used countermeasures against side-channel attacks is masking [1]. Masking protects secrets by splitting a secret value into several shares via secret sharing and performing computations on those shares, so that the leakage of any subset of intermediate values does not reveal the underlying secret. Applications of masking include the digital signature scheme Raccoon [2], which was submitted to the NIST Post-Quantum Cryptography Standardization process, as well as Masked ML-DSA [3]–[5], a masked variant of ML-DSA [6], among many others. The notion of noninterference is commonly used to formalize the security of masked algorithms in the ISW probing model [1]. However, proving noninterference by hand is errorprone, and several flaws have been identified in manual security proofs for masked algorithms [7], [8]. To avoid such errors, formal verification of probing security has been studied in recent years [9]–[20]. B. Formal Verification via Separation Logic Probabilistic separation logic [21] is a recently developed formal verification method for reasoning about probabilistic programs, including cryptographic algorithms. This is a variant This work was supported by JST K Program Grant Number JPMJKP24U2; JSPS KAKENHI Grant Number JP25H00446, JP25K21183.

of separation logic [22], which is a Hoare-style logic that can reason about separation of resources using the separating conjunction ϕ∗ψ. Together with the frame rule, the separating conjunction enables local reasoning, which is particularly useful for modular verification of large programs. Separation logic was originally introduced to reason about mutable data structures in imperative programs [22], but it has since been applied in a variety of contexts beyond memory separation. Probabilistic separation logic interprets the separating conjunction as probabilistic independence between random variables and has been applied to verify input independence properties of cryptographic algorithms, such as the one-time pad and private information retrieval. Several extensions of probabilistic separation logic have been proposed [23]–[28], including Lilac [29], which supports reasoning about conditional independence. Masking can be viewed as a generalization of the one-time pad, which strongly suggests that probabilistic separation logic is a natural framework for verifying probing security. However, to the best of our knowledge, none of these logics has been used to verify probing security of masked algorithms. C. Connection Between Simulator-Based Security Notions and Conditional Independence In this work, we establish a connection between simulatorbased definitions of probing security and conditional independence, enabling the use of probabilistic separation logic for formal verification of probing security. In cryptography, many security notions, including noninterference, are defined via simulators. To understand the connection between such simulator-based definitions and conditional independence, consider a cryptographic algorithm (Fig. 1a) and an adversary who attempts to learn some secret information from the input by observing information leaked during the execution of the algorithm. In this situation, three kinds of information are involved: (i) secret information A in the input, (ii) public (non-secret) information B in the input, which is not directly observed by the adversary, and (iii) information C observed by the adversary. To formalize the requirement that the adversary cannot learn A from C, simulator-based security definitions postulate the existence of a simulator that can compute C solely from B, without access

secret input A

cryptographic algorithm

public input B

output C observed by adversary

(a) A cryptographic algorithm with input and output

public input B

simulator

observed output C

(b) Simulator-based formulation

A⊥C|B (c) Conditional-independence-based formulation

Fig. 1: Two formulations of security: simulator-based formulation and conditional-independence-based formulation.

to A (Fig. 1b). If such a simulator exists, then the adversary cannot distinguish the real execution from the simulated one. Consequently, although the adversary may obtain some information about B, it is impossible to learn A. We rephrase this simulator-based definition in terms of conditional independence (Fig. 1c). Suppose that A, B, and C are random variables. Given A and B, the probability distribution of C generated by the cryptographic algorithm (Fig. 1a) corresponds to the conditional probability distribution Pr[C|A, B]. On the other hand, given only B, the probability distribution of C generated by the simulator (Fig. 1b) corresponds to Pr[C|B]. The simulator-based definition requires that these two probability distributions are equal: Pr[C|A, B] = Pr[C|B]. This is exactly the definition of conditional independence of A and C given B, denoted by A ⊥ C | B. This connection leads to the idea of verifying simulator-based security notions by proving conditional independence properties using probabilistic separation logic that can reason about conditional independence. D. Contributions In this paper, we formalize the connection between simulator-based definitions of probing security and conditional independence within the semantic framework of Lilac [29]. Although the underlying idea of this connection is conceptually simple, its formalization in Lilac is technically non-trivial. This difficulty stems from the fact that Lilac models probabilistic independence using independent combination, rather than the standard construction based on product probability spaces. The relationship between these two notions of independence has been studied in [30]; however, that work does not address the semantics of the conditioning modality defined via disintegration. Consequently, establishing the desired connection in Lilac requires a careful measure-theoretic argument. Although technically demanding, this formalization pays off by making it possible to reason about probing security directly within Lilac. Our main theorem (Theorem V.1) states that the simulator-based definition of noninterference is equivalent to the conditional independence property expressed as a Hoare triple in Lilac. By the main theorem, to verify probing security of a masked algorithm, it suffices to prove the corresponding conditional independence property using proof rules of Lilac. Moreover, we provide additional proof rules for Lilac that are necessary to verify probing security of masked algorithms but are not provided in the original Lilac paper [29]. In

particular, we show that semi-graphoid axioms for conditional independence hold in Lilac. These additional rules enhance the verification power of Lilac for reasoning about probing security. We also consider proof rules related to composability of noninterference properties and capture them in Lilac. Composability is an important aspect and has been studied in prior works [9], [31]. In contrast to prior works, our composability rules focus on (I, O)-noninterference, which is a basic building block for the definitions of t-noninterference and its variants. We demonstrate the effectiveness of our approach by verifying non-interference of the R EFRESH algorithm [8], [9], multiplication [1], and A DD R EP N OISE [32] using Lilac: the first two are fundamental building blocks for masked algorithms, and the last one is a key component of the security proof of Raccoon [2]. The contributions of this work are summarized as follows: • We establish a connection between existence of simulators and conditional independence, which allows us to use probabilistic separation logics for conditional independence, such as Lilac, to verify probing security. • We provide additional proof rules for Lilac that are necessary to verify probing security of masked algorithms. In particular, we show that semi-graphoid axioms for conditional independence hold in Lilac. We also provide proof rules related to composability of noninterference. • We demonstrate the effectiveness of our approach by verifying non-interference of the R EFRESH algorithm [8], [9], multiplication [1], and A DD R EP N OISE [32] using Lilac. II. OVERVIEW A. Simulator-Based Security Notions and Probabilistic Independence We illustrate the connection between simulator-based security notions and probabilistic independence, using the one-time pad encryption as an example. Example II.1 (One-time pad). Suppose that a plaintext message is given as an element M in a finite abelian group K. The following program implements the one-time pad encryption: OTP(M ) K ← unif K; C ← ret (M − K); ret C

Here, unif K is the uniform distribution over K, and C ← ret (M − K) means deterministic assignment of the value M − K to the variable C. The programming language used in this paper will be formally introduced later in Section III-A. a) Simulator-based formulation of security: We can formulate the security of the one-time pad using simulators. In this setting, a simulator is defined as a program Sim(OTP) that simulates the distribution of C computed by OTP(M ) without knowing M . If such a simulator exists, then the adversary cannot learn any information about M because the adversary cannot distinguish the real execution from the simulated one, which does not depend on M . Concretely, a valid simulator for the one-time pad can be given as a program that uniformly samples a random element from K as the ciphertext: Sim(OTP) := unif K. b) Independence-based formulation: Shannon’s perfect secrecy is a well-known security notion for encryption schemes [33] and defined as the independence between the plaintext M and the ciphertext C. This captures the intuition that observing the ciphertext C does not provide any information about the plaintext M . In fact, the independence of M and C is equivalent to the existence of a simulator described above. To express and verify such independence properties of randomized programs, we can use probabilistic separation logic [21], [29]. In probabilistic separation logic, sources of randomness are treated as resources. We have a basic assertion own E, which asserts ownership of a random variable E, and the separating conjunction ϕ ∗ ψ expresses that the random variables mentioned in ϕ and those in ψ are independent. Therefore, we can express the independence between two random variables X and Y as own X ∗ own Y . Using probabilistic separation logic, the probabilistic independence between the plaintext M and the ciphertext C can be written as a Hoare triple {own M } OTP(M ) {C. own M ∗ own C} This states that, starting from an initial random variable satisfying the precondition own M , after executing the program OTP(M ), the resulting random variable satisfies the postcondition own M ∗ own C where C is a random variable bound to the output of the program. To prove that the above Hoare triple holds, we can use the proof rules of probabilistic separation logic, which have been already demonstrated in [21, Section 5.1.2] for the one-time pad. In this case, we do not need conditional independence since the simulator does not take any input. However, as we will see below, conditional independence becomes necessary when we consider simulators that take some input, such as in the case of non-interference verification. B. Noninterference of Masked Programs and Conditional Independence Masking is a widely used countermeasure against sidechannel attacks [1], where a secret value is split into several

shares via secret sharing and computations are performed on those shares. A bit more formally, let X be a secret value represented as an element in a finite abelian group K. The secret value X is split into t + 1 shares K∋X

7→

X = (X (0) , . . . , X (t) ) ∈ Kt+1

such that the secret value X can be recovered as the sum of all shares X = X (0) + · · · + X (t) , but any proper subset of the shares does not reveal any information about X. The value t is called the masking order. An algorithm is said to be masked if secret input values are represented using such shares, and the algorithm operates on such shares. Example II.2. Consider adding two values X and Y in a finite abelian group K. A masked implementation of the addition with two shares (t = 1) is given as follows. M ASKEDA DD(X (0) , X (1) , Y (0) , Y (1) ) Z (0) ← ret (X (0) + Y (0) ); Z (1) ← ret (X (1) + Y (1) ); ret (Z (0) , Z (1) ) It is straightforward to see that the output shares Z (0) and Z (1) represent the sum Z = X + Y of two input values. Masked algorithms are expected to be secure against sidechannel attacks, since the leakage of at most t shares does not reveal any information about the underlying secret value. This security notion is formalized by t-noninterference [10], which we informally describe below. a) Simulator-based formulation of t-noninterference: In Example II.2, the secret values X and Y remain secure even if an adversary can only guess at most t input shares for each of X and Y . This intuition is formalized as a security definition for masked algorithms, by considering a simulator that takes t input shares as its input and outputs the values that are probed by an adversary. In the t-probing model, an adversary is allowed to choose arbitrary probe locations and observe up to t intermediate values during the execution of the program. A masked algorithm is said to be t-noninterfering if, for any choice of at most t probes, there exists a simulator that, given at most t input shares, can simulate the values observed at those probes. The existence of such a simulator ensures that the adversary cannot learn any information about the secret values from the probed values, since the adversary cannot guess input shares that are not given to the simulator. b) Conditional-independence-based formulation: Similarly to the case of the one-time pad, we can rephrase the definition of t-noninterference in terms of conditional independence. Specifically, we consider the conditional independence between the input shares not in the simulator’s input and the probed values, given the input shares provided to the simulator. It turns out that this conditional independence is equivalent to the simulator-based definition of t-noninterference, which we will formally state in Theorem V.1. To reason about such conditional independence properties of masked programs, we can use an extension of probabilistic separation logic for conditional independence, namely, Lilac

[29]. In Lilac, the conditional independence between random variables X and Y given Z can be expressed as a formula Cz←Z (own X ∗ own Y ) where the conditioning modality Cz←Z represents conditioning on the random variable Z. Using Lilac, the conditional independence required for tnoninterference of a masked program M ASKEDA DD can be expressed as follows: for each choice of probe locations1 P ⊆ {X (0) , X (1) , Y (0) , Y (1) , Z (0) , Z (1) } such that |P| ≤ t = 1, there exists a choice of at most one input share X ⊆ X and Y ⊆ Y from each of X = (X (0) , X (1) ) and Y = (Y (0) , Y (1) ) such that |X |, |Y| ≤ |P| and the following Hoare triple holds. { own(X, Y) } M ASKEDA DD(X, Y) { Z.

(own(X \ X , Y \ Y) ∗ own P) }

(x,y)←(X ,Y)

Here, X\X denotes the tuple of variables that are in X but not in X . This Hoare triple states that the information observed by the adversary (or the output of the simulator) P is independent of the secret input X \ X and Y \ Y, given the public input X and Y provided to the simulator. Once we have established the connection between simulator-based definitions of t-noninterference and conditional independence, it remains to show that the above Hoare triple holds for each choice of probe locations P. This can be done by applying the proof rules of Lilac. For example, consider the case when the adversary probes the output share P = {Z (0) }. Then, we can choose X = {X (0) } and Y = {Y (0) } as the input shares to be given to the simulator. Using Lilac’s proof rules, we can derive the following Hoare triple: { own(X, Y) } M ASKEDA DD(X, Y) { Z.

(own(X (1) , Y (1) ) ∗ own Z (0) ) } (1)

(x,y)←(X (0) ,Y (0) )

A bit more concretely, this is proved as follows. We first use the rule for Hoare triples in Fig. 4 to derive the following Hoare triple.

own(X, Y) ∗ Z (0) = X (0) + Y (0) ⊢

M ASKEDA DD(X, Y) (0) as

(0)

}

(2)

Here, = stands for the almost-sure equality between two random variables. By the consequence rule (H-C ONSEQ), it remains to show that the postcondition of (2) implies that of (1). This is done by using the proof rules for Lilac formulas. Several proof rules are provided in [29]; however, they are not sufficient to derive the desired entailment. Therefore, we introduce several new rules for Lilac formulas in Section VI, including the following rule. ϕ ∗ (own(X, Y )) ⊢ C (ϕ ∗ own Y ) x←X

1 Without loss of generality, we may assume that the set of probes P does not contain input shares: P ⊆ {Z (0) , Z (1) }.

(own(X (1) , Y (1) ) ∗ Z (0) = X (0) + Y (0) )

(x,y)←(X (0) ,Y (0) )

Under the conditioning modality, (X (0) , Y (0) ) are equal to as deterministic values (x, y). Thus, we can conclude that Z (0) = x + y is conditionally independent of (X (1) , Y (1) ), as desired. As we have seen in the above example, we can use Lilac to prove t-noninterference of masked programs, given (1) the connection between simulator-based definitions and conditional independence and (2) additional proof rules for Lilac formulas, such as the weak union rule. In the subsequent sections, we will formally present such results. We will also show more examples of masked programs and their security proofs using Lilac in Section VII. III. P RELIMINARIES A. A Probabilistic Programming Language: APPL We define a probabilistic programming language called APPL following [29]. 1) Syntax: Expressions are defined as follows. E

x | X | T | F | k | i | if E0 then E1 else E2 | (E1 , . . . , En ) | proji E | E1 op E2

Here, x is a deterministic variable, X is a random variable, k ∈ K is a constant in a finite abelian group K, and i is a natural number. The constant T (resp. F) represents the boolean value true (resp. false). The symbol op ranges over binary operations, including group operations such as + and −; boolean operations such as ∧ and ∨; and comparison operations such as =, and ̸=. Expressions are typed in a standard way. Types are defined as follows. A, B

{ own(X, Y) } { Z.(own(X, Y)) ∗ Z

This is a generalization of the weak union property of conditional independence, which states W ⊥ (X, Y ) | Z implies W ⊥ Y | (X, Z) for random variables W , X, Y , and Z. We will prove the soundness of this rule in Proposition VI.1. Using this rule, we can have the following entailment:

bool | K | index | A1 × · · · × An

We have base types bool, K, and index for boolean values, elements of the group K, and indices for for loops, respectively. Types also include product types A1 × · · · × An . The empty product type (n = 0) is written as unit. Typing judgements for expressions are given in the form of Γ; ∆ ⊢ E : A where Γ = x : A1 , . . . , xm : Am is a typing context for deterministic variables and ∆ = X : A1 , . . . , Xn : An is a typing context for random variables. Typing rules are standard [29] and omitted here. APPL programs are defined as follows. L, M, N :=

ret E | X ← M ; N | unif K | for (X ← E; i ← nstart . . . nend ) {M }

In the for-loop for (X ← E; i ← nstart . . . nend ) {M }, i is the loop index variable ranging from nstart to nend . The

variable X is initialized with E at the beginning of the loop, and in each iteration, X is updated with the result of M . The final value of X after the last iteration is returned as the result of the for-loop. One might expect the for-loop to be written as X ← E; for i ← nstart · · · nend {M }. However, we adopt the above syntax because X is bound by the for-loop construct. In sequential composition X ← M ; N and for-loops, we often bind multiple variables at once. Formally, when the result of M is a tuple, we define (X, Y ) ← M ; N as syntactic sugar for Z ← M ; N [proj1 Z/X, proj2 Z/Y ] where Z is a fresh variable, and similarly for for-loops. In many examples in this paper, we also use indexed variables such as Xi and Xi,j and consider programs such as XE ← M ; N where E is an expression of type index. We do not include conditional branching as a primitive construct in APPL. However, they can be defined as syntactic sugar using conditional branching for expressions. if E then M else N := X ← M ; Y ← N ; ret (if E then X else Y ) Since APPL does not cause computational effects other than randomness, this definition is semantically equivalent to the standard conditional branching construct. Typing judgments for programs are given in the form of ∆ ⊢ M : GA where ∆ is a typing context for random variables. Here, GA represents a type of distributions over values of type A. Typing rules are shown in Fig. 2. 2) Semantics: Each type A is interpreted as a measurable space JAK in the standard way. Note that all base types are interpreted as countably generated measurable spaces, which implies that any type is also interpreted as a countably generated measurable space. The interpretation of a context Γ = x : A1 , . . . , xm : Am is defined as the product measurable space JΓK = JA1 K × · · · × JAm K. Expressions Γ; ∆ ⊢ E : A are interpreted as functions JEK : JΓK → Meas(J∆K, JAK) where Meas(X, Y ) is the set of measurable functions from X to Y . Programs ∆ ⊢ M : GA are interpreted as Markov kernels, i.e., measurable functions that maps each element in J∆K to a probability measure over JAK: JM K ∈ Meas(J∆K, GJAK) Here, G is the Giry monad, which maps a measurable space to the measurable space of probability measures over it. Concrete definitions of the semantics are standard [29] and omitted. B. t-Probing Model and Noninterference In the t-probing model, an adversary is allowed to probe up to t internal or output values during the execution of a masked program where t is the order of masking. The adversary aims to guess secret information from the observed values, which is achieved if the adversary can guess more than t input shares. The notion of t-noninterference formalizes the security requirement in this setting. Suppose that X1 , . . . , Xn

(0)

(t)

are shared inputs where each Xi = (Xi , . . . , Xi ) is a tuple of t + 1 shares. A masked program M is said to be tnoninterfering (t-NI) if for any set of probes O with |O| ≤ t, there exists a subset Ii ⊆ Xi for each i such that |Ii | ≤ |O| and the values of probes in O can be simulated using only the input shares in I1 , . . . , In . Below, we rephrase the definitions of t-noninterference and related notions in terms of APPL programs. Suppose that we have an APPL program ∆ ⊢ M : GB where ∆ = X1 : A1 , . . . , Xm : Am and B = B1 × · · · × Bn . We assume that M is in the static single assignment (SSA) form so that each internal value computed in M is assigned to a unique variable name. Then, probes can be specified by a set of variables. We call variables X1 , . . . , Xm in the context ∆ the input variables of M . The output variables of M are variables bound to the output value of M and have type B. The output variables do not a priori occur in the program, but we often introduce them to refer to the output of M . The internal variables of M are variables occurring in M other than input variables. Later in Section IV, we will introduce Hoare triples to reason about APPL programs. A Hoare triple is given in the form {ϕ} M {Y.ψ} where ϕ is an assertion over input variables of M , Y is a tuple of variables bound to the output of M , and ψ is an assertion over both input variables and output variables Y. Hoare triples cannot refer to internal variables directly, but we can easily transform a given APPL program to expose internal variables as output variables. For example, the APPL program X : K ⊢ Y ← ret X + X; ret Y + X : K has one input variable X and one internal variable Y , and outputs Y + X. Let Z be an output variable bound to the output. Hoare triples {ϕ} Y ← ret X + X; ret Y + X {Z.ψ} for this program can refer to X and Z, but not to Y directly. In this case, we can transform the program to X : K ⊢ Y ← ret X +X; Z ← ret Y + X; ret (Y, Z) : K × K so that both Y and Z are accessible as output variables. In general, given a program M , we can construct a program M ♯ that exposes all internal variables as output. ∆ ⊢ M : GB

7→

∆ ⊢ M ♯ : G(Bint × B)

Here, Bint is the type of the tuple of all internal variables of M . Of course, the transformed program M ♯ is defined so that M is semantically equal to (Y, Z) ← M ♯ ; ret Z where Y and Z are tuples of internal and output variables, respectively. In what follows, we assume that APPL programs are appropriately transformed so that internal variables are accessible as parts of output variables. Then, probes can be specified by output variables only. Now, we define the notion of noninterference for APPL programs. Throughout the paper, we write a tuple of variables X = (X1 , . . . , Xm ) in bold font and often identify the tuple with the set {X1 , . . . , Xm } for notational convenience. Definition III.1. Let ∆ ⊢ M : GB be an APPL program where ∆ = X1 : A1 , . . . , Xm : Am and B = B1 × · · · × Bn . We write I = {X1 , . . . , Xm } for the set of input variables and

∅; ∆ ⊢ E : A ∆ ⊢ ret E : GA

∆ ⊢ M : GA ∆, X : A ⊢ N : GB ∆ ⊢ X ← M ; N : GB

∆ ⊢ unif K : GK

∅; ∆ ⊢ E : A ∆, i : index, X : A ⊢ M : GA ∆ ⊢ for (X ← E; i ← ns . . . ne ) {M } : GA Fig. 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

Here, ∆I is the restriction of ∆ to variables in I and BO = Q Yi ∈O Bi is the restriction of B to components in O. We call such a program Sim(M ) a simulator for M with input I and output O. The notion of t-noninterference [10] for masked algorithms is defined using (I, O)-NI. Definition III.2 (t-NI). Suppose that the input variables of the APPL program M consist of shared values X1 , . . . , Xn where (0) (t) each Xi = (Xi , . . . , Xi ) is a tuple of t + 1 shares, and suppose that the output variables are O = {Y1 , . . . , Ym }. We say that M is t-noninterfering (t-NI) if for any set of probes O ⊆ O with |O| ≤ t, there exist subsets X1 ⊆ X1 , . . . , Xn ⊆ Xn such that |Xi | ≤ |O| for each i, and M is (X1 ∪ · · · ∪ Xn , O)-noninterfering.

is (X1 ∪ · · · ∪ Xn ∪ Y, O)-noninterfering. A strong version of NIU (SNIU) can be defined similarly. There are other variants of t-NI in the literature, such as noninterference with public outputs (NIo) [35] and probe isolating noninterference (PINI) [31]. Although we do not give their definitions here, they can also be defined via (I, O)-NI. Since (I, O)-NI is the basis of various notions of noninterference, we mainly focus on verifying (I, O)-NI for APPL programs in the rest of this paper. IV. L ILAC : A S EPARATION L OGIC FOR C ONDITIONAL I NDEPENDENCE We briefly review the syntax and semantics of Lilac [29], a probabilistic separation logic that can reason about conditional independence. Syntax: Formulas of Lilac are defined as follows. ⊤ | ⊥ | ϕ ∧ ψ | ϕ ∨ ψ | ∀x.ϕ | ∃x.ϕ

ϕ, ψ :=

| ∀rv X.ϕ | ∃rv X.ϕ | ϕ ∗ ψ | ϕ −∗ ψ | own E | □ ϕ |

x:A←E

There are several variants of t-noninterference proposed in the literature. One of such variants is strong noninterference (SNI) [9], which exhibits a better composability property. This variant is also defined based on (I, O)-NI. Definition III.3 (t-SNI). Suppose the same setting as in Definition III.2. Let Oint ⊆ O be the set of exposed internal variables, which are not used as input to subsequent programs. We say that M satisfies t-strong noninterference (t-SNI) if for any set of probes O ⊆ O with |O| ≤ t, there exist subsets X1 ⊆ X1 , . . . , Xn ⊆ Xn such that for each i, |Xi | ≤ |O∩Oint | and M is (X1 ∪ · · · ∪ Xn , O)-noninterfering. Another variant is noninterference with unshared input (NIU) [34], which generalizes ordinary noninterference by allowing unshared inputs in addition to shared inputs. Definition III.4 (t-NIU). Suppose that the input variables of the APPL program M consist of shared inputs X1 , . . . , Xn and unshared inputs Y = (Y1 , . . . , Ym ) where each Xi = (0) (t) (Xi , . . . , Xi ) is a tuple of t + 1 shares. Let O be the set of output variables of M . We say that M is t-noninterfering with unshared input (t-NIU) if for any set of probes O ⊆ O with |O| ≤ t, there exist subsets X1 ⊆ X1 , . . . , Xn ⊆ Xn and Y ⊆ Y such that |Xi | ≤ |O| for each i, |Y| ≤ |O|, and M

ϕ | E ∼ µ | E1 = E2 | wp(M, X : A.ϕ)

Here, µ := unif K | · · · is a distribution, including the uniform distribution unif K over a finite group K. Formulas defined above assert propositions about random variables and the ownership of sources of randomness. Below we briefly explain the intended meaning of each construct. The formula own E asserts the probabilistic ownership of the random variable E. The formula E ∼ µ asserts that the random variable E follows the distribution µ and that its probabilistic ownership is as held. The formula E1 = E2 asserts that the random variables E1 and E2 are almost surely equal. The separating conjunction ϕ ∗ ψ asserts that ϕ and ψ own disjoint, probabilistically independent sources of randomness and that ϕ holds for one part and ψ holds for the other part. The conditioning modality Cx←E ϕ, which is one of the main features of Lilac, asserts that ϕ holds when conditioning on the value of E being x. The weakest precondition wp(M, X : A.ϕ) for program M and postcondition ϕ asserts that after executing M and binding the result to the random variable X, the formula ϕ holds. The persistence modality [36] is denoted by □ ϕ, which asserts that ϕ holds without owning any source of randomness. There are two types of quantifiers: the standard quantifiers ∀x.ϕ and ∃x.ϕ for deterministic variables, and the random variable quantifiers ∀rv X.ϕ and ∃rv X.ϕ for random variables.

For example, own X ∗ own Y means that the random variables X and Y are independent. Conditional independence of X and Y given Z is expressed as Cz←Z (own X ∗own Y ). Typing judgements for Lilac formulas are denoted by Γ; ∆ ⊢ ϕ where Γ is a typing context for deterministic variables and ∆ is a typing context for random variables. Typing rules are standard [29] and omitted here. We write ϕ ⊢ ψ if ϕ entails ψ in Lilac. We also write ⊢ ψ when ϕ is ⊤. If both ϕ ⊢ ψ and ψ ⊢ ϕ hold, then we write ϕ ⊣⊢ ψ. The semantics of the entailment relation is given later. Inference rules for the entailment relation are shown in Fig. 3. Most of the rules are taken from [29], but we also include some rules that are not explicitly in [29] but are easily proved to be valid. Later in Section VI, we also provide several non-trivial additional rules that are not in [29]. To reason about APPL programs, Hoare triples are defined in Lilac as follows. {ϕ} M {X.ψ}

□(ϕ −∗ wp(M, X : A.ψ))

This is semantically equivalent to ϕ ⊢ wp(M, X : A.ψ). Inference rules for Hoare triples are shown in Fig. 4. Semantics: We briefly explain the semantics of Lilac formulas [29]. The semantics of separating conjunction in Lilac is based on the notion of Kripke resource monoids (KRMs) [37]. A KRM is a partially ordered partial commutative monoid (M, 1, ·, ⊑) such that the order relation ⊑ is compatible with the monoid product. To capture probabilistic independence of random variables, Lilac uses a specific KRM defined on the set of probability spaces on a fixed sample space Ω. Definition IV.1. Let (Ω, ΣΩ ) be the Hilbert cube [0, 1]N with the standard Borel σ-algebra. We define a KRM Mind = (M, 1, ·, ⊑) as follows. • The underlying set Ω is the set of probability spaces P = (Ω, F, µ) over the sample space Ω where F ⊆ ΣΩ is a σalgebra and µ : F → [0, 1] is a probability measure. We often omit Ω and simply write (F, µ) for a probability space in M. • The monoid product · is defined by the independent combination of probability spaces: given a pair of probability spaces (F, µ) and (G, ν) in Mdisint , their independent combination (F , µ) · (G, ν) is a (necessarily unique) probability space (H, λ) such that H is the smallest σalgebra containing both F and G, and λ witnesses the independence of F and G, i.e., for any F ∈ F and G ∈ G, λ(F ∩ G) = µ(F ) · ν(G). The unit element is the trivial probability space ({∅, Ω}, µ). • The order relation (F , µ) ⊑ (G, ν) is defined by F ⊆ G and µ = ν|F where ν|F is the restriction of ν to F. Conditioning modalities in Lilac are interpreted by disintegrations [38]. To ensure the existence of disintegrations, Lilac formulas are interpreted using a submonoid Mdisint ⊆ Mind that imposes technical conditions on probability spaces (see [29, Section 3] for details). The semantics of Lilac formulas Γ; ∆ ⊢ ϕ is defined by the relation γ, D, P |= ϕ where γ ∈ JΓK is a valuation for

deterministic variables in Γ, D : Ω → J∆K is a measurable function representing a random variable environment for ∆, and P ∈ Mdisint is an element of the KRM of which the formula has ownership. Below, we write RV A := {D : Ω → A} for the set of random variables where A is a measurable space. We show the semantics of important constructs; the semantics of other constructs can be found in [29].2 γ, D, (F, µ) |= own E if JEK(γ) ◦ D is F-measurable where ◦ is function composition. • γ, D, (F, µ) |= E ∼ ν if JEK(γ) ◦ D is F-measurable and the pushforward measure (JEK(γ) ◦ D)∗ µ is ν. • γ, D, P |= ϕ ∗ ψ if γ, D, P1 |= ϕ and γ, D, P2 |= ψ for some P1 , P2 ∈ Mdisint such that P1 · P2 ⊑ P. ′ • γ, D, (F, µ) |= Cx:A←E ϕ if for any (ΣΩ , µ ) ⊒ (F, µ) ′ and any µ -disintegration {νx }x∈JAK with respect to JEK(γ) ◦ D, it holds that γ, D, (F , νx |F ) |= ϕ for almost every x ∈ JAK. Here, the disintegration {νx }x∈JAK intuitively represents the conditional distribution given the value of JEK(γ) ◦ D ∈ RVJAK. • γ, D, P |= wp(M, X : A.ϕ) if for all Pf and µ such that Pf · P ⊑ (ΣΩ , µ) and for all D ∈ RVJ∆e K, there exist X ∈ RVJAK, P ′ , and µ′ such that Pf · P ′ ⊑ (ΣΩ , µ′ ), γ, (D, X), P ′ |= ϕ, and the following two distributions are equal:   ! ω ← µ; ω ← µ′ ;   v ← JM K(D(ω)); = ret (De (ω), D(ω), X(ω)) ret (De (ω), D(ω), v) •

Finally, we define the entailment relation ϕ ⊢ ψ as follows. ∀γ.∀D.∀P.

γ, D, P |= ϕ

=⇒

γ, D, P |= ψ

V. N ONINTERFERENCE AND C ONDITIONAL I NDEPENDENCE In this section, we present our main result that characterizes noninterference as conditional independence expressed by Lilac Hoare triples. Let ∆ ⊢ M : GB be an APPL program where ∆ = X1 : A1 , . . . , Xm : Am and B = B1 × · · · × Bn . Let I and O be subsets of input and output variables, respectively; i.e., I ⊆ {X1 , . . . , Xm } and O ⊆ {Y1 , . . . , Yn } where Y1 , . . . , Yn are output variables of M . We show that (I, O)-NI is equivalent to the following Hoare triple. {own ∆} M {Y. C (own(∆ \ I) ∗ own O)} x←I

Here, we identify ∆ with the tuple of all input variables (X1 , . . . , Xm ). Without loss of generality, we assume that input and output variables are {X1 , X2 } and {Y1 , Y2 }, respectively, and consider ({X1 }, {Y1 })-NI. 2 The semantics of almost-sure equality presented in [29] contains a flaw and was later corrected in the arXiv version. In this paper, we adopt the corrected semantics. In fact, our results do not depend heavily on the semantics of almost-sure equality itself, since we use it primarily through syntactic inference rules, whose soundness has been proved under the corrected semantics.

C-E NTAIL

ϕ⊢ψ C ϕ⊢ C ψ

x←E

C-I NDEP

C-S UBST

own E ∗ ϕ ⊢ C ϕ

own X ⊢ C (X = x)

x←E

C-OWN

own E ⊢ C own E x←E

x←X

□-E LIM

□ϕ ⊢ ϕ

x←E

C-A ND -D ISTRIBUTIVE

C-U NIF

C (ϕ ∧ ψ) ⊣⊢ C ϕ ∧ C ψ

own X ∧ C (Y ∼ unif K) ⊢ own X ∗ (Y ∼ unif K)

x←X

U NIF -B IJECTION

□-C ONJ

ϕ ∧ □ψ ⊢ ϕ ∗ □ψ

T RANSFER -OWN

Γ; X : K ⊢ E : K E is bijective in X X ∼ unif K ⊢ E ∼ unif K

own E1 ∧ (E1 = E2 ) ⊢ own E2

Fig. 3: Selected inference rules for Lilac formulas [29]. See Fig. 12 in the appendix for a more comprehensive list of rules. We omit obvious structural rules like commutativity and associativity of the separating conjunction ∗. Note that Lilac is an affine separation logic, and thus ϕ ∗ ψ ⊢ ϕ holds. H-L ET

H-U NIF

H-R ET

{⊤} unif K {X.X ∼ unif K}

{Q[E/X]} ret E {X.Q}

{P } M {X.Q} ∀rv X.{Q} N {Y.R} {P } X ← M ; N {Y.R} H-C ONSEQ

H-F OR

P ⊢ P′

∀i : index.∀rv X : A.{I(i, X)} M {X ′ .I(i + 1, X ′ )} {I(ns , E)} for (X ← E; i ← ns . . . ne ) {M } {X.I(ne + 1, X)}

{P ′ } M {X.Q′ } {P } M {X.Q}

Q′ ⊢ Q

H-F RAME

{P } M {X.Q} X∈ /R {P ∗ R} M {X.Q ∗ R} Fig. 4: Inference rules for Hoare triples in Lilac [29] Theorem V.1. Let X1 : A1 , X2 : A2 ⊢ M : G(B1 × B2 ) be an APPL program. We have {own(X1 , X2 )} M {(Y1 , Y2 ). C (own X2 ∗ own Y1 )} x←X1

X2 . By (4), the output distribution of (Y1 , Y2 ) ← M ; ret Y1 also satisfies the same conditional independence. Therefore, we have the desired Hoare triple for M .

(3) if and only if there exists a simulator X1 : A1 ⊢ Sim(M ) : GB1 such that the following equation holds.

The idea of the proof itself is simple, but its formal proof requires several technical lemmas on disintegrations and the semantics of Lilac. Details are given in Appendix B.

X1 : A1 , X2 : A2 ⊢ Sim(M ) = (Y1 , Y2 ) ← M ; ret Y1 : GB1 (4)

VI. A DDITIONAL P ROOF RULES FOR L ILAC

We give a proof sketch of Theorem V.1. We write Pr[Y |X] for the conditional probability distribution of Y given X. Proof sketch. ( =⇒ ): By the Hoare triple for M , the input (X1 , X2 ) and the output (Y1 , Y2 ) satisfy X2 ⊥ Y1 | X1 , which implies Pr[Y1 |X1 , X2 ] = Pr[Y1 |X1 ]. Since Pr[Y1 |X1 , X2 ] is the output probability distribution of (Y1 , Y2 ) ← M ; ret Y1 for given inputs X1 and X2 , the equation Pr[Y1 |X1 , X2 ] = Pr[Y1 |X1 ] implies that (Y1 , Y2 ) ← M ; ret Y1 does not actually depend on X2 . Therefore, we define Sim(M ) as follows where v : A2 is an arbitrary value. Sim(M )

X2 ← ret v; (Y1 , Y2 ) ← M ; ret Y1 (5)

( ⇐= ): If a simulator Sim(M ) satisfying (4) exists, then we have X2 ⊥ Y1 | X1 because Sim(M ) does not depend on

The original Lilac paper [29] provides several proof rules, which are summarized in Fig. 3. However, these rules are not sufficient for our purpose. In this section, we present additional proof rules that we use in Section VII. In particular, we show that semi-graphoid axioms for conditional independence hold in Lilac. We also provide composability rules for (I, O)-NI properties as proof rules for Lilac. A. Semi-Graphoid Axioms for Conditional Independence In the classical probability theory, conditional independence is known to satisfy the graphoid axioms [39]. Here, we show that a subset of the graphoid axioms, called semi-graphoid axioms, hold in Lilac. Using the conventional notation X ⊥ Y | Z meaning conditional independence of random variables X and Y given Z, the semi-graphoid axioms are stated as follows.

Proposition VI.3. Theorem V.1 holds when we replace {P } M {X.Q} with {{P }} M {{X.Q}}. In particular, (I, O)-NI property of an APPL program M can be written as follows by Theorem V.1. {{⊤}} M {{Y. C (own(∆ \ I) ∗ own O)}} x←I

C (own X ∗ own Y ) ⊢ C (own Y ∗ own X)

C. Monotonicity

C (own W ∗ own(X, Y )) ⊢ C (own W ∗ own X)

By the simulator-based definition of (I, O)-NI, it is straightforward to see that if M is (I, O)-NI, I ⊆ I ′ , and O ⊇ O′ , then M is also (I ′ , O′ )-NI. This gives rise to the following proof rule.

z←Z

C (own W ∗ own(X, Y )) ⊢ C

z←Z

C (own W ∗ own X)

z←Z y←Y

C (own W ∗ own X) ∧ C

z←Z

C (own W ∗ own Y )

z←Z x←X

⊢ C (own W ∗ own(X, Y )) z←Z

We show these entailments hold in Lilac’s semantics. By CE NTAIL and C-A ND -D ISTRIBUTIVE, it suffices to show these entailments without the outermost conditioning modalities Cz←Z . The symmetry axiom is immediate from the commutativity of the separating conjunction. The decomposition axiom is also straightforward because own(X, Y ) ⊢ own X holds. The weak union and contraction axioms are non-trivial, but they also hold as stated in the following proposition. The proofs are given in Appendix C-A. Proposition VI.1. The following entailments hold. G EN -W EAK -U NION

ϕ ∗ own(X, Y ) ⊢

C (ϕ ∗ own(X, Y ))

x:A←X

C ONTRACTION

(own W ∗ own X) ∧ C (own W ∗ own Y ) x←X

⊢ own W ∗ own(X, Y )

Note that we slightly generalize the statements of the weak union. It subsumes C-I NDEP as a special case when Y is a trivial random variable over a singleton set and also subsumes C-OWN. When verifying noninterference properties of the examples in Section VII, we often use G EN -W EAK -U NION to introduce conditioning modalities. B. Hoare Triples with Ownership Assertions When we write Hoare triples for APPL programs ∆ ⊢ M : GA, we often want to assume own ∆ in the precondition. Writing own ∆ explicitly in every Hoare triple is tedious, so we introduce a syntactic sugar for this purpose. For each APPL program ∆ ⊢ M : GA, we define {{P }} M {{X.Q}} as syntactic sugar for {P ∧ own ∆} M {X.Q ∧ own ∆ ∧ own X}. We can use this syntactic sugar in the same way as the original Hoare triples. Proposition VI.2. All rules in Fig. 4 is sound when we replace all occurrences of {P } M {X.Q} with {{P }} M {{X.Q}}.

I ⊆ I′ ⊆ ∆ Y ⊇ O ⊇ O′ {{⊤}} M {{Y. C (own(∆ \ I) ∗ own O)}} x←I

{{⊤}} M {{Y. C (own(∆ \ I ′ ) ∗ own O′ )}} ′ x←I

This is a consequence of Theorem V.1, but we can also prove it from semi-graphoid axioms. Lemma VI.4. Suppose I ⊆ I ′ ⊆ ∆ and X ⊇ O ⊇ O′ . Then, we have the following. (∆ \ I) ⊥ O | I

=⇒

(∆ \ I ′ ) ⊥ O′ | I ′

Proof. Without loss of generality, we show the case where both ∆ = {X1 , X2 , X3 } and Y = (Y1 , Y2 , Y3 ) consist of three variables, and we have I = {X1 }, I ′ = {X1 , X2 }, O = {Y1 , Y2 }, and O′ = {Y1 }. Then, we have the following. X2 , X3 ⊥ Y1 , Y2 | X1 =⇒ X2 , X3 ⊥ Y1 | X1

by decomposition

=⇒ X3 ⊥ Y1 | X1 , X2

by weak union

D. Composability for Sequential Composition Suppose we have two APPL programs ∆ ⊢ M : GA and ∆, X : A ⊢ N : GB whose output variables are tuples X and Y, respectively. Consider the sequential composition ∆ ⊢ X ← M ; N : GB. ∆ M

If M is (IM , OM )-NI and N is (IN , ON )-NI with OM ⊇ IN ∩ X, then the sequential composition X ← M ; N is (IM ∪ (IN ∩ ∆), ON )-NI. We formalize this composability property as a proof rule in Lilac as follows. By monotonicity of (I, O)-NI (Section VI-C), it suffices to consider the case where OM = IN ∩ X and IM = IN ∩ ∆: M is (I, OM )-NI N is (I ∪ OM , ON )-NI X ← M ; N is (I, ON )-NI This gives rise to the following proof rule. {{⊤}} M {{X. C (own(∆\I) ∗ own OM )}} w←I

{{⊤}} N {{Y.

(own(∆\I, X\OM ) ∗ own ON )}}

(w,x)←(I,OM )

{{⊤}} X ← M ; N {{Y. C (own(∆\I) ∗ own ON )}} x←I

Similarly to monotonicity, this is a consequence of Theorem V.1, but we can also prove it from semi-graphoid axioms. Lemma VI.5. We have the following. (∆\I ⊥ OM | I) ∧ (∆\I, X\OM ⊥ ON | I, OM ) =⇒ ∆\I ⊥ ON | I E. Composability for For-Loops Consider a for-loop for (Y ← E; i ← ns . . . ne ) {M } where Y = (Y1 , . . . , Yn ) is a tuple of random variables, and ∆, i : index, Y : B ⊢ M : B. ∆ M

i = ns

···

i = ne

Let Ii ⊆ {1, . . . , n} be a subset of indices for each i = ns , . . . , ne + 1, and let I be a subset of ∆. If (i) for each i = ns , . . . , ne , M is (I ∪ {Yj }j∈Ii , {Yj′ }j∈Ii+1 )-NI where Y′ = (Y1′ , . . . , Yn′ ) is the output of M , and (ii) for each j ∈ Ins , free variables of Ej are in I, then the for-loop is (I, {Yj }j∈Ine +1 )-NI where Y = (Y1 , . . . , Yn ) is used as the output of the for-loop. This gives the following proof rule. own Y|ns ⊢ own E|ns {{⊤}} M {{Y′ . C (own(∆\I, Y\Y|i ) ∗ own Y′ |i+1 )}} (x,y)←(I,Y|i )

{{⊤}} for (Y ← E; i ← ns . . . ne ) {M } {{Y. C (own(∆\I) ∗ own Y|ne +1 )}} x←I

Here, we write Y|i for the tuple (Yj )j∈Ii and similarly for Y′ |i and E|i . We can prove this either from Theorem V.1 or by semi-graphoid axioms. F. Weakening When composing programs, a component program often uses only a subset of input variables. The situation can be illustrated as follows. M

X Z

Y Z

In this case, we want to reason about the component program M with the subset X of input variables and then extend the result to the whole set of input variables X, Z. Specifically, suppose that M is (I, O)-NI where I ⊆ X and O ⊆ Y. Then, we want to conclude that M is also (I ∪ Z, O ∪ Z)-NI for any Z ⊆ Z. This gives rise to the following proof rule. {{⊤}} M {{Y. C (own(X \ I) ∗ own O)}} x←I

∀rv Z.{{⊤}} M {{Y. C (own(X\I, Z\Z) ∗ own(O, Z))}} (x,z)←(I,Z)

Note that Z need not be independent of X. Hence, this is a different local reasoning principle from the frame rule in probabilistic separation logic.

A DD R EP N OISE ER({Vi }i∈[l] , ρ) {Xi,0 }i∈[l] ← {Vi }i∈[l] for i = 1, . . . , l do for irep = 1, . . . , r do Yi,irep ← M INI A DD R EP N OISE(Xi,irep −1 , ρi,irep ) Xi,irep ← R EFRESH(Yi,irep ) return {Xi,r }i∈[l] Fig. 5: AddRepNoiseER [32] in conventional pseudocode. Here, [l] = {1, 2, . . . , l}, and ρ = {ρi,irep }i∈[l],irep ∈[r] where ρi,irep = {ρi,irep ,j }j∈{0,...,t} and ρi,irep ,j : K. M INI A DD R EP N OISE(V, ρ) for j = 0, . . . , t do X j ← V j + ρj return X Fig. 6: MiniAddRepNoise in conventional pseudocode.

VII. A PPLICATIONS TO P ROBING S ECURITY Raccoon [2] is a masking-friendly lattice-based signature scheme. Raccoon employs a sum-of-uniforms distribution as its noise source to address the difficulty of generating discrete Gaussian noise in a side-channel-resistant manner. An algorithm called A DD R EP N OISE is used in Raccoon to add uniform noise to masked values. In this section, we demonstrate how Lilac can be used to prove the probing security of A DD R EP N OISE ER, a variant of A DD R EP N OISE that is used in the security proof of Raccoon [32]. The algorithm A DD R EP N OISE ER (Fig. 5) adds uniform noise ρi,irep ,j to each share Vij using M INI A DD R EP N OISE (Fig. 6), and then refreshes the shares using the R E FRESH algorithm (Fig. 8). This procedure is repeated r times for each of the l shared variables. The uniform noise ρi,irep ,j is sampled externally and provided to A DD R EP N OISE ER as an unshared input (ER stands for Explicit Randomness). Below, we prove that A DD R EP N OISE ER satisfies the t-SNIU property (Definition III.4), which plays a central role in the security proof of Raccoon [32]. Following [32, Lemma 6.1], the proof is divided into three parts. After proving the security of A DD R EP N OISE ER, we present another example in which we prove the t-SNI property of a masked multiplication algorithm [1]. A. t-NIU of M INI A DD R EP N OISE We first prove the noninterference property of M INI A D D R EP N OISE [32], which is a subroutine used in A DD R EP N OISE ER. The program in conventional pseudocode is shown in Fig. 6 and its APPL version with proof outline is shown in Fig. 7. This algorithm takes a shared input V = (V 0 , . . . , V t ) and an unshared input ρ = (ρ0 , . . . , ρt ). The output is X = (X 0 , . . . , X t ), and there are no internal variables. Theorem VII.1. Let O ⊆ X be a set of probed variables shared unshared such that |O| ≤ t. We define I = IMARN (O) ∪ IMARN (O) shared j j unshared by IMARN (O) := {V | X ∈ O} and IMARN (O) :=

R EFRESH(A) for i = 0, . . . , t do C0i ← Ai for i = 0, . . . , t do for j = i + 1, . . . , t do Ri,j ← unif K i Cji ← Cj−1 + Ri,j j Ci+1 ← Cij − Ri,j return Ct = (Ct0 , . . . , Ctt )

{ own(V, ρ) } {I(0; 0) } for (X ← 0; j ← 0, . . . , t) { { I(j; X) } {⊤}

H-F RAME j

ret X[V + ρj /X ] as

{ X′ . X′ = X[V j + ρj /X j ] } as

Fig. 8: Algorithm R EFRESH [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.

{ X′ . X′ = X[V j + ρj /X j ] ∗ I(j; X) } ′

′

{ X . I(j + 1; X ) } } { X. I(t + 1; X) } { X.

(own(V \ I, ρ \ I) ∗ own O) }

C (v,r)←(V∩I,ρ∩I)

I(j; X)

own(V, ρ, X) ∗

∗ X =V +ρ k as

Since X j = v j + rj is deterministic, we have □ own X j for each X j ∈ O. Thus, we obtain the desired postcondition. Details of the proof are given in Appendix D-A.

k<j

Fig. 7: Algorithm M INI A DD R EP N OISE in APPL. Gray lines show the proof outline for Theorem VII.1. We apply the HF OR rule to the loop with the loop invariant I(j; X).

{ρj | X j ∈ O} (here, “MARN” stands for MiniAddRepNoise). Then, the following Hoare triple is derivable in Lilac, meaning that M INI A DD R EP N OISE is (I, O)-NI. {own(V, ρ)} j

for (X ← 0; j ← 0, . . . , t) { ret X[V + ρj /X ] } (own(V \ I, ρ \ I) ∗ own O)}

(v,r)←(V∩I,ρ∩I)

Proof sketch. The outline of the proof is shown in Fig. 7. It is straightforward to see that the following postcondition holds after executing the program by considering the loop invariant I(j; X) defined in the figure. as

(own V ∧ own ρ) ∗ X = V + ρ We can show that this implies the desired postcondition. By G EN -W EAK -U NION, we have the following entailment.

(own(V, ρ) ∗ X = V + ρ)

(v,r)←(V∩I,ρ∩I)

By C-S UBST, we also have the following entailment. ^ as as own(V, ρ) ⊢ (v j = V j ∧ rj = ρj ) C (v,r)←(V∩I,ρ∩I)

X j ∈O

Then, it follows that the following entailment holds. as

own(V, ρ) ∗ X = V + ρ ⊢

(v,r)←(V∩I,ρ∩I)

B. t-SNI of R EFRESH R EFRESH is an algorithm shown in Fig. 8 and used in masked algorithms to ensure noninterference [9], [32]. The input is a shared variable A = (A0 , . . . , At ), and the output is Ct = (Ct0 , . . . , Ctt ) such that Ct and A represent the same secret value. The internal variables are {Ri,j }0≤i<j≤t and {Cji }0≤i≤t,0≤j<t . Theorem VII.4. Consider R EFRESH in Fig. 8. Let O ⊆ {Ri,j | i, j ∈ {0, . . . , t}, i < j} ∪ {Cji | i, j ∈ {0, . . . , t}} be a set of probed variables such that |O| ≤ t. We define I = IRefresh (O) ⊆ {A0 , . . . , At } as follows. IRefresh (O)

own(V, ρ) ∗ X = V + ρ ⊢

Corollary VII.3. M INI A DD R EP N OISE is t-NIU. Proof. Immediate from Theorem VII.1.

{

Remark VII.2. As explained in Section III-B, reasoning about noninterference properties in our approach requires exposing internal variables. This typically does not undermine the local reasoning principle of separation logic, because the internal variables exposed in earlier steps are not used in subsequent steps. Moreover, the frame rule allows us to frame out postconditions concerning those internal variables. This is illustrated by the use of H-F RAME in Fig. 7.

(own(V \ I, ρ \ I) ∧

X j ∈O

X j = v j + rj )

{Ai | ∃j.Ri,j ∈ O ∨ ∃j < t.Cji ∈ O}

Then, the following Hoare triple is derivable in Lilac, meaning that R EFRESH is (I, O)-NI. {own A} R EFRESH {(C, R). C (own(A \ I) ∗ own O)} a←I

Proof sketch. The outline of the proof is shown in Fig. 9. It is straightforward to show that the following postcondition holds. own A ∗

∗ (R ∼ unif K) ∗ ∗(C = A + f (R)) i,j

i<j

i,j

i as j

where fji (R) is a function defined as follows. ( P − k<j Rk,i i fj (R) := P P − k<i Rk,i + i<k≤j Ri,k

i j

i≥j i<j

(6)

{ own A } { I(0, 1; (A, 0, . . . , 0), 0) } for ( (C′ , R′ ) ← ((A, 0, . . . , 0), 0); i ← 0, . . . , t ) { for ( (C, R) ← (C′ , R′ ); j ← i + 1, . . . , t ) { { I(i, j; C, R) } {⊤}

H-F RAME

S ← unif K; { S. S ∼ unif K } j i ret (C, R)[Cj−1 + S/Cji , Cij − S/Ci+1 , S/Ri,j ] as

j i , S/Ri,j ] } { (C′′ , R′′ ). S ∼ unif K ∗ (C′′ , R′′ ) = (C, R)[Cj−1 + S/Cji , Cij − S/Ci+1 as

j i , S/Ri,j ] ∗ I(i, j; C, R) } { (C′′ , R′′ ). S ∼ unif K ∗ (C′′ , R′′ ) = (C, R)[Cj−1 + S/Cji , Cij − S/Ci+1

{ (C′′ , R′′ ). I(i, j + 1; C′′ , R′′ ) } } } { (C, R). I(t, t + 1; C, R) } { (C, R). own A ∗

∗ (R ∼ unif K) ∗ ∗(C = A + f (R)) } i,j

i<j

i,j

i as j

i j

{ (C, R). C (own(A \ I) ∗ own O) } a←I

I(i, j; C, R)

own A ∗

∗C = A ∗ ∗ i

i as 0

(i′ ,j ′ )<lex (i,j) 0≤i′ <j ′ ≤t

′ ′ ′ as ′ ′ ′ as Ri′ ,j ′ ∼ unif K ∗ Cji′ = Ai + fji′ (R) ∗ Cij′ +1 = Aj + fij′ +1 (R)

Fig. 9: Algorithm R EFRESH in APPL. Here, R is a shorthand for the collection of random variables Ri,j , and C = (C0 , . . . , Ct ) where Ci = (Ci0 , . . . , Cit ) 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 fji (R) is a function defined in (6). We can derive the desired postcondition by translating the proof in [9] into Lilac. See Appendix D-B for details. Corollary VII.5. R EFRESH is t-SNI. Proof. By Theorem VII.4, for each set of probes O with |O| ≤ t, there exists a set of inputs I with |I| smaller than or equal to internal probes in O such that R EFRESH is (I, O)-NI. C. t-SNIU of A DD R EP N OISE with Explicit Randomness

tively. For each i and irep , we define Ji,irep ⊆ Yi,irep , shared unshared Ii,i ⊆ Xi,irep −1 , and Ii,i ⊆ ρi,irep as follows. rep rep Ji,irep

shared Refresh IRefresh (Ii,i ∪ Oi,i ) rep +1 rep

shared Ii,i rep

shared MARN IMARN (Ji,irep ∪ Oi,i ) rep

unshared Ii,i rep

shared MARN IMARN (Ji,irep ∪ Oi,i ) rep

shared := Here, we define Ii,r+1 ∅. Let I be defined as follows. [ k shared unshared I := {Vik | Xi,0 ∈ Ii,0 }∪ Ii,i rep i,irep

A DD R EP N OISE ER is shown in Fig. 5. Here, we write [l] = {1, 2, . . . , l}. The shared input is Vi = (Vi0 , . . . , Vit ) for i = 1, . . . , n, and the unshared input is ρ = {ρi,irep }i∈[l],irep ∈[r] where ρi,irep = {ρi,irep ,j }j∈{0,...,t} and ρi,irep ,j : K. For 0 t each i and irep , Xi,irep = (Xi,i , . . . , Xi,i ) and Yi,irep = rep rep 0 t (Yi,irep , . . . , Yi,irep ) are used as internal or output variables. We can prove that A DD R EP N OISE ER in Fig. 5 is t-SNIU by using the composability of NI discussed in Section VI. Theorem VII.6. Let O be a set of probed variables such that Refresh MARN |O| ≤ t. We write Oi,i and Oi,i for the subsets of O rep rep consisting of probed variables in the execution of R EFRESH and M INI A DD R EP N OISE in the (i, irep )-th iteration, respec-

Then, A DD R EP N OISE ER is (I, O)-NI. Proof. By using composability for sequential composition and for-loop with Theorem VII.4 and VII.1. Corollary VII.7. A DD R EP N OISE ER is t-SNIU. D. t-SNI of S EC M ULT The multiplication algorithm [1] is another basic building block for masked algorithms. In Fig. 10, S EC M ULT takes two shared inputs A = (A0 , . . . , At ) and B = (B 0 , . . . , B t ) t and returns a shared output Ct = (Ct0 , . . . , CtP ) such that t i Ct represents the product of A and B, i.e., i=0 Ct =

S EC M ULT(A, B) for i = 0, . . . , t do for j = 0, . . . , t do Pi,j ← Ai × B j 0 (C0 , . . . , C0t ) ← (P0,0 , . . . , Pt,t ) for i = 0, . . . , t do for j = i + 1, . . . , t do Qi,j ← unif K i Cji ← Cj−1 − Qi,j Ri,j ← Qi,j + Pi,j Si,j ← Ri,j + Pj,i j Ci+1 ← Cij + Si,j return Ct = (Ct0 , . . . , Ctt ) Fig. 10: Algorithm S EC M ULT in conventional pseudocode. Unlike the presentation in [9], our version computes Pi,j ← Ai × B j for all i, j in advance, since we need to assign a distinct variable name to each Ai × B j for the proof.

Pt Pt ( i=0 Ai ) × ( i=0 B i ). It is proved in [9] that S EC M ULT 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 variables.

define KQ , KS ⊆ {(i, j) | 0 ≤ i < j ≤ t} as follows. KQ := {(i, j) | Qi,j ∈ O ∨ Ri,j ∈ O} ∪ {(i, k) | Cji ∈ O, j < t, i < k} KS := {(i, j) | Si,j ∈ O} ∪ {(k, i) | Cji ∈ O, j < t, k < i} The set KC is defined so that (a) KC bijectively corresponds to the set {Cti ∈ O | ¬(∃j < t, Cji ∈ O)} and (b) for each (i′ , j ′ ) ∈ KC corresponds to Cti , the uniform random variable Qi′ ,j ′ occurs in gti (Q, S). We can define such KC because we have |O ∩ Ct | ≤ |Vi \ (KQ ∪ KS )| for each Cti ∈ O with no j < t such that Cji ∈ O, where Vi = {(k, i) | k < i} ∪ {(i, k) | i < k} is the indices of the free variables in gti (Q, S). We can then show that (a) {Cti ∈ O | ¬(∃j < t, Cji ∈ O)} can be “simulated” by sampling from the uniform distribution, (b) {Si,j | (i, j) ∈ KS \ KQ } can be “simulated” by sampling from the uniform distribution, and (c) the rest of the variables in O can be “simulated” from {Si,j | (i, j) ∈ KS \ KQ }, {Qi,j | (i, j) ∈ KQ }, and I ∪ J . In Lilac, (a) and (b) correspond to applying U NIF -B IJECTION, and (c) corresponds to applying T RANSFER -OWN. See Appendix D-C for details. Corollary VII.9. S EC M ULT is t-SNI.

I1 := {i | Pi,j ∈ O} ∪ {i | Cji ∈ O ∧ j < t} J1 := {j | Pi,j ∈ O} ∪ {i | Cji ∈ O ∧ j < t} (I2 , J2 ) := Add(I1 , J1 ; {(i, j) | Qi,j ∈ O ∨ Ri,j ∈ O}) (I3 , J3 ) := Add(I2 , J2 ; {(i, j) | Si,j ∈ O}) Here, for each I, J ⊆ {0, . . . , t} and K ⊆ {0, . . . , t}2 , Add(I, J; K) is the pair (I ′ , J ′ ) defined as follows. I ′ := I ∪ {i | (i, j) ∈ K ∧ i ∈ / I} ∪ {j | (i, j) ∈ K ∧ i ∈ I} ′ J := J ∪ {j | (i, j) ∈ K ∧ j ∈ / J} ∪ {i | (i, j) ∈ K ∧ j ∈ J} Let I := I3 , J := J3 , and I = {Ai | i ∈ I}, J = {B j | j ∈ J}. Then, S EC M ULT is (I ∪ J , O)-NI. Proof sketch. We rephrase the simulator-based proof in [9] as a conditional-independence-based proof in Lilac. We first apply the rules in Fig. 4 to obtain a postcondition that expresses how each variable is computed from the inputs and the random variables. This step is rather straightforward, and the proof sketch is shown in Fig. 11. Here, gji (Q, S) is defined as follows. (P Sk,i i≥j i gj (Q, S) := Pk<j (7) P i<j k<i Sk,i + i<k≤j Qi,k Then, we apply the H-C ONSEQ rule to obtain the desired postcondition, which is the non-trivial part of the proof. We divide (the indices of) the uniform random variables Q into four parts: KQ , KS \ KQ , KC , and the rest. Here, we

VIII. R ELATED W ORK a) Probabilistic separation logic: Probabilistic separation logic [21] is extended in various ways to support more expressive reasoning about probabilistic programs. Some works support reasoning about conditional independence, such as Lilac [29], DIBI [23], BaSL [24], and BlueBell [25]. Other works interpret separating conjunction in different ways: cryptographic probabilistic separation logic [27] interprets it as computational independence, while LINA [28] provides a separating conjunction for negative association. Probabilistic concurrent outcome logic (pcOL) [26] combines probabilistic separation logic with concurrent separation logic [40] to reason about probabilistic concurrent programs. Some of the above logics have been applied to verify cryptographic algorithms [21], [25], [27], [29]. However, none of these logics has been used to verify t-noninterference of masked algorithms. b) Formal verification of masked programs: Formal verification of probing security has been actively studied in recent years [9]–[20], [41], [42]. MASK V ERIF [10], [11] repeatedly substitute expressions in masked programs to prove noninterference, based on the fact that applying bijective functions f to uniform random variables X gives uniform random variables f (X) as well. Lilac has an inference rule (U NIF -B IJECTION) that captures this fact, which allows us to use the simulated their noninterference proof as a proof in Lilac. Substitutionbased approaches have also been used in [20]. Another line of work uses inference-based approaches [12]–[14], [41], [42], which infer distribution types for each intermediate values in masked programs.

{ own(A, B) } P ← for (P ← 0; i ← 0, . . . , t) { ′ for (P′ ← P; j ← 0, . . . , t) { ret P′ [Ai × B j /Pi,j ]}

};

∗P = A × B } { P. own(A, B) ∗ ∗ P = A × B ∗ I(0, 1; ((P ) , 0, . . . , 0), 0, 0, 0) } { P. own(A, B) ∗

i,j

t i,i i=0

i,j

(C, Q, R, S) ← for ((C, Q, R, S) ← (((Pi,i )ti=0 , 0, . . . , 0), 0, 0, 0); i ← 0, . . . , t) { for ((C′ , Q′ , R′ , S′ ) ← (C, Q, R, S); j ← i + 1, . . . , t) { { own(A, B) ∗

∗ P = A × B ∗ I(i, j; C , Q , R , S ) } as

i,j

′

i,j

Q′′i,j ← unif K; i

′′ ′′ ′′ ′′ C ′′ j ← ret (C ′ j−1 − Q′′i,j ); Ri,j ← ret (Q′′i,j + Pi,j ); Si,j ← ret (Ri,j + Pj,i ); C ′′ i+1 ← ret (C ′ i + Sj,i ); i

′′ ′ ′′ ′ ret (C′ , Q′ , R′ , S′ )[C ′′ j /C ′ j , C ′′ i+1 /C ′ i+1 , Q′′i,j /Q′i,j , Ri,j /Ri,j , Sj,i /Sj,i ]

{ (C′′ , Q′′ , R′′ , S′′ ). own(A, B) ∗

∗ P = A × B ∗ I(i, j + 1; C , Q , R , S ) } as

i,j

′′

i,j

} }; { own(A, B) ∗

∗ P = A × B ∗ I(t, t + 1; C, Q, R, S) } as

i,j

ret (P, C, Q, R, S)

∗ P = A × B ∗ ∗ Q ∼ unif K ∗ ∗ R = Q + P ∗ ∗ S = R + P ∗ ∗ C = P + g (Q, S) } as

{ (P, C, Q, R, S). own(A, B) ∗

i,j

j,i

i<j

{ (P, C, Q, R, S).

i,j as

i,j

i<j i as j

i,j

i<j

i j

i,i

(own(A \ I, B \ J ) ∗ own O) }

C (a,b)←(I,J )

I(i, j; C, Q, R, S)

C0 = (Pi,i )ti=0 ∗

∗

(i′ ,j ′ )<lex (i,j) 0≤i′ <j ′ ≤t

Qi′ ,j ′ ∼ unif K ∗ Ri′ ,j ′ = Qi′ ,j ′ + Pi′ ,j ′ ∗ Si′ ,j ′ = Ri′ ,j ′ + Pj ′ ,i′

′ ′ as ′ as j′ ∗ Cji′ = Pi′ ,i′ + gji ′ (Q, S) ∗ Cij′ +1 = Pj ′ ,j ′ + gi+1 ′ (Q, S) Fig. 11: Algorithm S EC M ULT 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 = (Ci0 , . . . , Cit ) for each i. Gray comments show the proof outline for Theorem VII.8, but we omit some straightforward proof steps for brevity. The function gji (Q, S) is defined as in (7). The loop invariant for the second loop is denoted as I(i, j; C, Q, R, S). When proving noninterference properties of masked algorithms, one must in principle consider all possible sets of probed variables O. This combinatorial explosion can be problematic, especially when pursuing algorithmic proof search [10]. However, in the setting of formal verification with an interactive theorem prover, this issue can be avoided by representing the set of probed variables symbolically. This is the approach adopted in this work. IX. C ONCLUSION AND F UTURE W ORK We have presented a method for formally verifying probing security using Lilac. We have shown that the simulator-based

definition of (I, O)-NI is equivalent to a Hoare triple in Lilac that asserts a certain conditional independence. We have also provided several proof rules that facilitate the verification of probing security and demonstrated their application to R EFRESH and A DD R EP N OISE ER. Our current results focus on the information-theoretic setting of probing security. As future work, we want to extend our approach to the computational setting by adopting the ideas from [27]. Implementing our method in an interactive theorem prover is another important direction for future work. We also want to explore applications of our method to the verification of other cryptographic algorithms, such as secure multi-party

computation protocols, since Theorem V.1 would be applicable to other security properties defined in terms of simulators as well. R EFERENCES [1] Y. Ishai, A. Sahai, and D. Wagner, “Private Circuits: Securing Hardware against Probing Attacks,” in Advances 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 [2] 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 [3] J.-S. Coron, F. Gérard, 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 [4] J.-S. Coron, F. Gérard, 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 [5] 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. [6] National Institute of Standards and Technology (US), “Module-latticebased 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 [7] T. Prest, “A Key-Recovery Attack Against Mitaka in the tProbing Model,” in Public-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 [8] J.-S. Coron, E. Prouff, M. Rivain, and T. Roche, “Higher-Order Side Channel Security and Mask Refreshing,” in Fast 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 [9] G. Barthe, S. Belaı̈d, F. Dupressoir, P.-A. Fouque, B. Grégoire, P.-Y. Strub, and R. Zucchini, “Strong Non-Interference and TypeDirected Higher-Order Masking,” in Proceedings 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/2976749.2978427 [10] G. Barthe, S. Belaı̈d, F. Dupressoir, P.-A. Fouque, B. Grégoire, 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-46800-5 18 [11] G. Barthe, S. Belaı̈d, G. Cassiers, P.-A. Fouque, B. Grégoire, and F.-X. Standaert, “maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults,” in Computer Security – ESORICS 2019, ser. Lecture Notes in Computer Science, vol. 11735. Cham: Springer International Publishing, 2019, pp. 300–318. [Online]. Available: https://link.springer.com/10.1007/978-3-030-29959-0 15 [12] J. Zhang, P. Gao, F. Song, and C. Wang, “SCInfer: RefinementBased Verification of Software Countermeasures Against SideChannel Attacks,” in Computer 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 [13] 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

[14] P. Gao, H. Xie, J. Zhang, F. Song, and T. Chen, “Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks,” in Tools 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.springer.com/10.1007/978-3-030-17462-0 9 [15] P. Gao, F. Song, and T. Chen, “Compositional Verification of FirstOrder 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 [16] 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. 2014. [Online]. Available: https://dl.acm.org/doi/10.1145/2685616 [17] J.-S. Coron, “Formal Verification of Side-Channel Countermeasures via Elementary Circuit Transformations,” in Applied 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 [18] R. Bloem, H. Gross, R. Iusupov, B. Könighofer, S. Mangard, and J. Winter, “Formal Verification of Masked Hardware Implementations in the Presence of Glitches,” in Advances in Cryptology – EUROCRYPT 2018, ser. Lecture Notes in Computer Science, vol. 10821. Cham: Springer International Publishing, 2018, pp. 321–353. [Online]. Available: https://link.springer.com/10.1007/978-3-319-78375-8 11 [19] D. Knichel, P. Sasdrich, and A. Moradi, “SILVER – Statistical Independence and Leakage Verification,” in Advances 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 [20] 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/ [21] 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 [22] J. Reynolds, “Separation logic: A logic for shared mutable data structures,” in Proceedings 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/ [23] J. Bao, S. Docherty, J. Hsu, and A. Silva, “A Bunched Logic for Conditional Independence,” in 2021 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/ [24] 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 [25] 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 [26] 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 [27] U. Dal Lago, D. Davoli, and B. M. Kapron, “On Separation Logic, Computational Independence, and Pseudorandomness,” in 2024 IEEE 37th Computer Security Foundations Symposium (CSF). Enschede, Netherlands: IEEE, Jul. 2024, pp. 80–95. [Online]. Available: https://ieeexplore.ieee.org/document/10664346/ [28] 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

[29] 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 [30] J. M. Li, J. Aytac, P. Johnson-Freyd, A. Ahmed, and S. Holtzen, “A Nominal Approach to Probabilistic Separation Logic,” in Proceedings 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 [31] 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/ [32] 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 [33] 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 [34] M. F. Esgin, T. Espitau, G. Niot, T. Prest, A. Sakzad, and R. Steinfeld, “plover: Masking-friendly hash-and-sign lattice signatures,” in Advances 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 [35] G. Barthe, S. Belaı̈d, T. Espitau, P.-A. Fouque, B. Grégoire, M. Rossi, and M. Tibouchi, “Masking the GLP Lattice-Based Signature Scheme at Any Order,” in Advances 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/10.1007/978-3-319-78375-8 12 [36] R. Jung, R. Krebbers, J.-H. Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer, “Iris from the ground up: A modular foundation for higherorder 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 [37] D. Galmiche, D. Méry, 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 [38] 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 [39] 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?” in Advances in Artificial Intelligence II, Seventh European Conference on Artificial Intelligence, ECAI 1986, Brighton, UK, July 20-25. North-Holland, 1986, pp. 357–363. [40] 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 [41] I. B. E. Ouahma, Q. Meunier, K. Heydemann, and E. Encrenaz, “Symbolic approach for side-channel resistance analysis of masked assembly codes,” in PROOFS 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 [42] 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 BASIC FACTS ABOUT P ROBABILITY T HEORY Let f : A → B be a measurable function between measurable spaces (A, ΣA ) and (B, ΣB ), and let µ be a probability measure on (A, ΣA ). The pushforward measure f∗ µ is the probability measure on (B, ΣB ) defined by (f∗ µ)(E) = µ(f −1 (E)) for any measurable set E ∈ ΣB . Let P be a predicate on a set X. The Iverson bracket [P ] is defined by ( 1 P is true [P ] = 0 otherwise. Definition A.1 (π-system). Let P ⊆ 2X be a nonempty collection of subsets of X. Then, P is a π-system if for all A, B ∈ P , we have A ∩ B ∈ P . Definition A.2 (λ-system). Let L ⊆ 2X be a nonempty collection of subsets of X. Then, L is a λ-system if: • X ∈ L. • If A, B ∈ L, then B \ A ∈ L. S∞ • If A1 ⊆ A2 ⊆ . . . is an increasing sequence in L, then i=1 Ai ∈ L. Theorem A.3 (Dynkin’s π-λ theorem). Let P be a π-system and L be a λ-system such that P ⊆ L. Then, the σ-algebra generated by P is contained in L. P ⊆ L =⇒ σ(P) ⊆ L We list a few criteria for two functions/Markov kernels to be almost everywhere equal. Lemma A.4. Let µ be a probability measure on (X, ΣX ) and f, g : (X, ΣX ) → [0, ∞] be measurable functions such that f (x) ≤ g(x) for any x ∈ X. Then, f and g are µ-almost everywhere equal if and only if Ex∼µ f (x) = Ex∼µ g(x) . Lemma A.5. Let f, g : (X, ΣX ) → [0, ∞] be measurable functions and µ be a probability measure on (X, ΣX ). Then, f and g are µ-almost everywhere equal if and only if for any measurable set E ∈ ΣX , we have the following. Ex∼µ [x ∈ E] · f (x) = Ex∼µ [x ∈ E] · g(x) Proof. The only-if part is obvious. For the if part, let E< = {x ∈ X : f (x) < g(x)}. If E< is non-negligible, then we have Ex∼µ [x ∈ E< ] · f (x) < Ex∼µ [x ∈ E< ] · g(x) , which contradicts the assumption. Similarly, we can define E> = {x ∈ X : f (x) > g(x)} and obtain a contradiction if E> is non-negligible. Therefore, {x ∈ X : f (x) ̸= g(x)} = E< ∪ E> is negligible. Lemma A.6. Assume that (Y, ΣY ) is a countably generated σ-algebra. Let f, g : (X, ΣX ) → G(Y, ΣY ) be Markov kernels and µ be a probability measure on (X, ΣX ). Then, f and g are µ-almost everywhere equal if and only if for any measurable set E ∈ ΣX and F ∈ ΣY , we have Ex∼µ [x ∈ E] · f (x)(F ) = Ex∼µ [x ∈ E] · g(x)(F ) . If B is a basis of ΣY (i.e., σ(B) = ΣY ), then we can restrict F to be in B. Proof. The only-if part is obvious. For the if part, let {Bm }m∈N be a countable basis of ΣY . Without loss of generality, we assume that {Bm }m∈N is a π-system. By Lemma A.5, for any m, f (−)(Bm ) and g(−)(Bm ) are µ-almostTeverywhere equal, that is, Sm := {x ∈ X | f (x)(Bm ) = g(x)(Bm )} satisfies µ(Sm ) = 1. Now, we show that for any x ∈ m∈N Sm and any T F ∈ ΣY , we have f (x)(F ) = g(x)(F ). For any x ∈ m∈N Sm , it is easy to see that {F ∈ ΣY | f (x)(F ) = g(x)(F )} is a λ-system containing {Bm }m∈N . By the Dynkin’s π-λ theorem, for any F ∈ ΣY , we have f (x)(F ) = g(x)(F ). The last claim follows because the following set is a λ-system. {F ∈ ΣY | Ex∼µ [x ∈ E] · f (x)(F ) = Ex∼µ [x ∈ E] · g(x)(F ) } Definition A.7 (disintegration). Let (A, ΣA , µ) and (B, ΣB , λ) be probability spaces, and f : A → B be a measurable function. We say that {νy }y∈B is a disintegration of µ if y 7→ νy is a Markov kernel from B to A that satisfies the following conditions [38]: • For λ-almost all y ∈ B, we have νy ({x | f (x) = y}) = 1. Equivalently, Ey∼λ νy ({x | f (x) = y}) = 1. • The probability measure defined by E 7→ Ey∼λ νy (E) coincides with µ. Equivalently, Ey∼λ Ex∼νy g(x) = Ex∼µ g(x) for any measurable function g : A → [0, ∞].

We often consider the case where λ = f∗ µ, in which case we say that {νy }y∈B is a µ-disintegration with respect to f . By the first property of disintegration, we have the following lemma. Lemma A.8. Consider the setting in Definition A.7. For any measurable function g : A × B → [0, ∞], for λ-almost all y ∈ B, we have Ex∼νy g(x, f (x)) = Ex∼νy g(x, y) . Proof. For νy -almost all x ∈ A, we have g(x, f (x)) = g(x, y). Disintegrations are unique up to almost everywhere equality. Proposition A.9. Consider the setting in Definition A.7. If {νy }y∈B and {νy′ }y∈B are disintegrations, then νy and νy′ are equal for λ-almost all y ∈ B. Proof. By the properties of disintegration, for any measurable set E ∈ ΣB and F ∈ ΣA , we have the following equality. Ey∼λ [y ∈ E] · νy (F ) = Ex∼µ [f (x) ∈ E] · [x ∈ F ] = Ey∼λ [y ∈ E] · νy′ (F ) By Lemma A.6, νy and νy′ are equal for λ-almost all y ∈ B. B P ROOF OF T HEOREM V.1 To prove Theorem V.1, we prepare several lemmas. The following lemma relates the conditional independence formula Cx←X (own Y ∗own Z) and the conditional independence in terms of product probability measures. Lemma B.1. Let ·; X : A, Y : B, Z : C ⊢ Cx←X (own Y ∗ own Z) be a Lilac formula. We have γ, D, (F, µ) ⊨ Cx←X (own Y ∗ own Z) if and only if for any (ΣΩ , µ′ ) ⊒ (F, µ) and µ′ -disintegration {νx }x with respect to X, for almost all x, we have Y −1 (ΣB ) ∪ Z −1 (ΣC ) ⊆ F and Y∗ νx ⊗ Z∗ νx = (Y, Z)∗ νx . Here, ΣB and ΣC is the σ-algebra on JBK and JCK, respectively; and ⊗ is the product probability measure. Proof. By definition of γ, D, (F, µ) ⊨ Cx←X (own Y ∗ own Z), it suffices to show that for any (ΣΩ , µ′ ) ⊒ (F, µ), any µ′ -disintegration {νx }x with respect to X, and any x, we have γ, D, (F, νx |F ) ⊨ own Y ∗ own Z

⇐⇒

Y −1 (ΣB ) ∪ Z −1 (ΣC ) ⊆ F and Y∗ νx ⊗ Z∗ νx = (Y, Z)∗ νx

(8)

⇐⇒ Y −1 (ΣB ) ∪ Z −1 (ΣC ) ⊆ F and Y∗ νx ⊗ Z∗ νx = (Y, Z)∗ νx

(9)

Here, (8) and (9) follow from the following facts: −1 • (8): Since ΣB and ΣC are countably generated, so are Y (ΣB ) and Z −1 (ΣC ). • (9): By definition of product measurable spaces, we have Y∗ νx ⊗ Z∗ νx = (Y, Z)∗ νx if and only if for any measurable sets E ∈ ΣB and F ∈ ΣC , we have (Y∗ νx ⊗ Z∗ νx )(E × F ) = (Y, Z)∗ νx (E × F ). Note here that we have the following equations. (Y∗ νx ⊗ Z∗ νx )(E × F ) = (Y∗ νx )(E) · (Z∗ νx )(F ) = νx (Y −1 (E)) · νx (Z −1 (F )) (Y, Z)∗ νx (E × F ) = νx (Y −1 (E) ∩ Z −1 (F )) In the semantics of conditioning modalities in Lilac, one needs to take a probability distribution over the common sample space Ω. This requires assigning an arbitrary probability distribution to the region outside the domain of interest, but the following lemma ensures that this choice does not essentially affect the semantics. ′ Lemma B.2. Let µ, µ′ be probability measures on ΣΩ . Let D = (DX , DY ) and D′ = (DX , DY′ ) be random variables ′ ′ ′ D, D ∈ RVJ∆K where ∆ = X : A, Y : B. If D∗ µ = D∗ µ , then for any µ-disintegration {νx }x∈A with respect to DX ′ and any µ′ -disintegration {νx′ }x∈A with respect to DX , for D∗ µ-almost all x and for any E ∈ ΣB , we have νx (DY−1 (E)) = ′−1 ′ νx (DY (E)).

Proof. By Lemma A.6, it suffices to show that for any measurable set E ∈ ΣB and F ∈ ΣA , we have ′ ′ −1 ′ ) µ′ [x ∈ F ] · ν (D Ex∼(DX )∗ µ [x ∈ F ] · νx (DY−1 (E)) = Ex∼(DX x Y (E)) . ∗ By D∗ µ = D∗′ µ′ , it suffices to prove Ex∼(DX )∗ µ [x ∈ F ] · νx (DY−1 (E)) = P(x,y)∼D∗ µ [x ∈ F ∧ y ∈ E]. This is proved as follows. P(x,y)∼D∗ µ [x ∈ F ∧ y ∈ E] = Pω∼µ [DX (ω) ∈ F ∧ DY (ω) ∈ E] = Ex∼(DX )∗ µ Eω∼νx [DX (ω) ∈ F ] · [DY (ω) ∈ E] = Ex∼(DX )∗ µ [x ∈ F ] · νx (DY−1 (E)) By Lemma B.2, we have the following lemma. ′ ′ Lemma B.3. Let ∆ = X : A, Y : B, Z : C and D = (DX , DY , DZ ), D′ = (DX , DY′ , DZ ) be random variables such that ′ ′ ′ ′ (DX , DY , DZ ), (DX , DY , DZ ) ∈ RVJ∆K. Let µ, µ be probability measures on ΣΩ such that D∗ µ = D∗′ µ′ . Let F , F ′ ⊆ ΣΩ ′ be σ-algebras such that (DY , DZ ) is F-measurable and (DY′ , DZ ) is F ′ -measurable. Then, we have

γ, D, (F, µ|F ) ⊨ C (own Y ∗ own Z) x←X

⇐⇒

γ, D′ , (F ′ , µ′ |F ′ ) ⊨ C (own Y ∗ own Z) x←X

Proof. By symmetry, it suffices to prove that if γ, D, P ⊨ Cx←X (own Y ∗own Z), then γ, D′ , P ′ ⊨ Cx←X (own Y ∗own Z). By unfolding the definition, we have γ, D′ , P ′ ⊨ Cx←X (own Y ∗ own Z) if and only if for any µ′ -disintegration {νx′ }x with −1 −1 ′ respect to DX , we have for D∗′ µ′ -almost all x, and for any E ∈ ΣB and F ∈ ΣC , we have D′ Y (E) ∩ D′ Z (F ) ∈ F ′ and ′ ′ −1 ′ −1 ′ ′ −1 ′ ′ −1 νx (D Y (E) ∩ D Z (F )) = νx (D Y (E)) · νx (D Z (F )). Fix a µ-disintegration {νx }x with respect to DX . By γ, D, P ⊨ Cx←X (own Y ∗ own Z) and Lemma B.2, we have the following equation for almost all x. −1

−1

′ −1 νx′ (D′ Y (E) ∩ D′ Z (F )) = νx′ ((DY′ , DZ ) (E × F ))

= νx ((DY , DZ )−1 (E × F )) −1 = νx (DY−1 (E) ∩ DZ (F )) −1 = νx (DY−1 (E)) · νx (DZ (F )) ′−1 = νx′ (DY′−1 (E)) · νx′ (DZ (F ))

Therefore, we have γ, D′ , P ′ ⊨ Cx←X (own Y ∗ own Z). Lemma B.4. For any APPL program ∆ ⊢ M : GA, we have {own ∆} M {X. own ∆ ∧ own X} where own ∆ is shorthand for own(X1 , . . . , Xn ) when ∆ = X1 : A1 , . . . , Xn : An . Proof. By induction on the structure of M . • ret E: Since ∅; ∆ ⊢ E : A, we have own ∆ ⊢ own E by FV-OWN . H-R ET H-C ONSEQ •

{own ∆ ∧ own E} ret E {X. own ∆ ∧ own X} {own ∆} ret E {X. own ∆ ∧ own X}

X ← M; N: {own ∆ ∧ own X} N {Y. own ∆ ∧ own X ∧ own Y } {own ∆} M {X. own ∆ ∧ own X} {own ∆ ∧ own X} N {Y. own ∆ ∧ own Y } H-L ET {own ∆} X ← M ; N {Y. own ∆ ∧ own Y } H-C ONSEQ

•

unif K: H-U NIF

{⊤} unif K {X.X ∼ unif K} {own ∆} unif K {X. own ∆ ∗ X ∼ unif K} H-C ONSEQ {own ∆} unif K {X. own ∆ ∧ own X} H-F RAME

•

for (X ← E; i ← ns . . . ne ) {M }: Let I(i, X) := own ∆ ∧ own X. {own ∆ ∧ own X} M {X ′ . own ∆ ∧ own X ∧ own X ′ } {own ∆ ∧ own X} M {X ′ . own ∆ ∧ own X ′ } H-F OR {own ∆ ∧ own E} for (X ← E; i ← ns . . . ne ) {M } {X. own ∆ ∧ own X} H-C ONSEQ {own ∆} for (X ← E; i ← ns . . . ne ) {M } {X. own ∆ ∧ own X} H-C ONSEQ

Here, we use FV-OWN to show own ∆ ⊢ own E. To prove the ( =⇒ ) direction of Theorem V.1, we prepare several lemmas. In classical probability theory, X and Y are independent if and only if Pr[Y | X] = Pr[Y ]. The following lemma states a similar characterization for the Lilac formula own X ∗ own Y in terms of disintegrations. Lemma B.5. Let X : A, Y : B ⊢ own X ∗ own Y be a Lilac formula. We have γ, D, (F, µ) ⊨ own X ∗ own Y if and only if X and Y are F-measurable, and for any (ΣΩ , µ′ ) ⊒ (F, µ) and µ′ -disintegration {νx }x∈JAK with respect to X, we have Y∗ νx = Y∗ µ for almost all x ∈ JAK. Proof of Lemma B.5. The only if direction follows from the proof of C-I NDEP in [29, Lemma B.27]. To prove the if direction, it suffices to show µ(X −1 (E) ∩ Y −1 (F )) = µ(X −1 (E)) · µ(Y −1 (F )) for any measurable sets E ∈ ΣJAK and F ∈ ΣJBK . This is proved as follows.

µ(X −1 (E) ∩ Y −1 (F )) = Ex∼X∗ µ Eω∼νx [X(ω) ∈ E] · [Y (ω) ∈ F ] = Ex∼X∗ µ [x ∈ E] · Eω∼νx [Y (ω) ∈ F ] = Ex∼X∗ µ [x ∈ E] · Y∗ νx (F ) = Ex∼X∗ µ [x ∈ E] · Y∗ µ(F ) = Y∗ µ(F ) · Ex∼X∗ µ [x ∈ E] = µ(Y −1 (F )) · µ(X −1 (E))

Let M be a program with input variables X and output variables Y . The following lemma states that any disintegration that represents the conditional distribution Pr[Y | X] is almost everywhere equal to the distribution of the output of M given the input X. Lemma B.6. Let ∆ ⊢ M : GA be an APPL program, D ∈ RVJ∆K be a random variable, and (ΣΩ , µ) ∈ Mdisint . If a random variable Y ∈ RVJAK and (ΣΩ , µM ) ∈ Mdisint satisfy the following equation:   ! ω ← µ; ω ← µM ;   y ← JM K(D(ω)); = ret (D(ω), Y (ω)) ret (D(ω), y) then, for any µM -disintegration {νx }x∈J∆K with respect to D and for almost all x ∈ J∆K, we have Y∗ νx

JM K(x).

Proof of Lemma B.6. We apply Lemma A.6 to Y∗ νx and JM K(x). Note first that we have D∗ µM = D∗ µ. We show Ex∼D∗ µM [x ∈ E] · νx (Y −1 (F )) = Ex∼D∗ µ [x ∈ E] · JM K(x)(F ) for any measurable sets E ∈ ΣA and F ∈ ΣB . This is proved as follows: Ex∼D∗ µM [x ∈ E] · νx (Y −1 (F )) = Ex∼D∗ µM [x ∈ E] · Eω∼νx [Y (ω) ∈ F ] = Ex∼D∗ µM Eω∼νx [x ∈ E] · [Y (ω) ∈ F ] = Ex∼D∗ µM Eω∼νx [D(ω) ∈ E] · [Y (ω) ∈ F ] = Eω∼µM [D(ω) ∈ E] · [Y (ω) ∈ F ] = E(x,y)∼(D,Y )∗ µM [x ∈ E] · [y ∈ F ] = Ex∼D∗ µ Ey∼JM K(x) [x ∈ E] · [y ∈ F ] = Ex∼D∗ µ [x ∈ E] · Ey∼JM K(x) [y ∈ F ] = Ex∼D∗ µ [x ∈ E] · JM K(x)(F )

Given a pair of random variables (X, Y ), we can consider two types of disintegrations: one is joint disintegrations with respect to the pair (X, Y ) and the other is iterated disintegrations with respect to X and then Y . We consider the relationship between these two types of disintegrations. Lemma B.7. Let (Ω, ΣΩ , µ) be a probability space, and X : Ω → A and Y : Ω → B be random variables. Suppose that {νx }x∈A is a µ-disintegration with respect to X. For any g : A × B → R, we have the following equality. Ex∼X∗ µ Ey∼Y∗ νx g(x, y) = E(x,y)∼(X,Y )∗ µ g(x, y) Proof. Ex∼X∗ µ Ey∼Y∗ νx g(x, y) = Ex∼X∗ µ Eω∼νx g(x, Y (ω)) = Ex∼X∗ µ Eω∼νx g(X(ω), Y (ω)) = Eω∼µ g(X(ω), Y (ω)) = E(x,y)∼(X,Y )∗ µ g(x, y)

by Lemma A.8 by Definition A.7

Lemma B.8. Let (Ω, ΣΩ , µ) be a probability space, and X : Ω → A and Y : Ω → B be random variables. Suppose that {νx }x∈A is a µ-disintegration with respect to X, and {(νx )y }y∈B is a νx -disintegration with respect to Y . If (x, y) 7→ (νx )y is a Markov kernel, i.e., (x, y) 7→ (νx )y (E) is measurable for any measurable set E ∈ ΣΩ , then {(νx )y }(x,y)∈A×B is a µ-disintegration with respect to (X, Y ). Proof.

•

For (X, Y )∗ µ-almost all (x, y), it follows that Eω∼(νx )y [(X(ω), Y (ω)) = (x, y)] = 1

holds because E(x,y)∼(X,Y )∗ µ Eω∼(νx )y [(X(ω), Y (ω)) = (x, y)] = Ex∼X∗ µ Ey∼Y∗ νx Eω∼(νx )y [(X(ω), Y (ω)) = (x, y)] = Ex∼X∗ µ Ey∼Y∗ νx Eω∼(νx )y [(X(ω), y) = (x, y)] = Ex∼X∗ µ Ey∼Y∗ νx Eω∼(νx )y [X(ω) = x] = Ex∼X∗ µ Eω∼νx [X(ω) = x]

by Lemma B.7 by Lemma A.8

=1 •

We show Eω∼µ f (ω) = E(x,y)∼(X,Y )∗ µ Eω∼(νx )y f (ω) for any measurable function f : Ω → [0, ∞]. Eω∼µ f (ω) = Ex∼X∗ µ Eω∼νx f (ω) = Ex∼X∗ µ Ey∼Y∗ νx Eω∼(νx )y f (ω) = E(x,y)∼(X,Y )∗ µ Eω∼(νx )y f (ω)

The following lemma states that a joint disintegration can be seen as an iterated disintegration. Lemma B.9. Let (Ω, ΣΩ , µ) be a probability space with countably generated σ-algebra, and X : Ω → A and Y : Ω → B be random variables. Suppose that {νx,y }(x,y)∈A×B is a µ-disintegration with respect to (X, Y ), and {νx }x∈A is a µ-disintegration with respect to X. Then {νx,y }y∈B is a νx -disintegration with respect to Y for X∗ µ-almost all x. Proof of Lemma B.9. • We show Ey∼Y∗ νx Eω∼νx,y [Y (ω) = y] = 1 for almost all x. We use Lemma B.7. Ex∼X∗ µ Ey∼Y∗ νx Eω∼νx,y [Y (ω) = y] = E(x,y)∼(X,Y )∗ µ Eω∼νx,y [Y (ω) = y] =1

•

Using Lemma A.6, we show that F 7→ Ey∼Y∗ νx νx,y (F ) and νx are equal for almost all x. Ex∼X∗ µ [x ∈ E] · Ey∼Y∗ νx νx,y (F ) Ex∼X∗ µ Ey∼Y∗ νx [x ∈ E] · νx,y (F ) = E(x,y)∼(X,Y )∗ µ [x ∈ E] · νx,y (F ) = E(x,y)∼(X,Y )∗ µ Eω∼νx,y [X(ω) ∈ E] · [ω ∈ F ] = Eω∼µ [X(ω) ∈ E] · [ω ∈ F ] = Ex∼X∗ µ Eω∼νx [X(ω) ∈ E] · [ω ∈ F ] = Ex∼X∗ µ [x ∈ E] · νx (F )

Proof of Theorem V.1 ( =⇒ ). To show that the simulator (5) satisfies (4), it suffices to show that X1 : A1 , X2 : A2 ⊢ (Y1 , Y2 ) ← M ; ret Y1 : GB1 does not actually depend on X2 . We prove by contradiction. Let M ′ := (Y1 , Y2 ) ← M ; ret Y1 . Suppose that there exist a1 ∈ JA1 K and a2 , a′2 ∈ JA2 K such that JM ′ K(a1 , a2 ) ̸= JM ′ K(a1 , a′2 ). By assumption and the rules in Fig. 4, we have the following Hoare triple: {own X1 ∧ own X2 } M ′ {Y1 . C (own X2 ∗ own Y1 )} x←X1

Suppose that the input distribution is chosen so that (X1 , X2 ) is uniformly distributed over {(a1 , a2 ), (a1 , a′2 )}. By the above Hoare triple, the output Y1 satisfies Cx←X1 (own X2 ∗ own Y1 ). Formally, let µ be a probability measure on ΣΩ and D ∈ RVJX1 : A1 , X2 : A2 K be such that D∗ µ is the uniform distribution over {(a1 , a2 ), (a1 , a′2 )}. Then, there exists Y1 ∈ RVJB1 K, P ′ , and µ′ with P ′ ⊑ (ΣΩ , µ′ ) such that   ! ω ← µ; ω ← µ′ ;   (y1 , y2 ) ← JM K(D(ω)); = ret (D(ω), Y1 (ω)) ret (D(ω), y1 ) and γ, (D, Y1 ), P ′ ⊨ Cx←X1 (own X2 ∗own Y1 ). Let {νx1 }x1 ∈JA1 K be a µ′ -disintegration with respect to X1 . Since (X1 )∗ µ′ = (X1 )∗ µ = δa1 , we have µ′ = νa1 and thus γ, (D, Y1 ), P ′ ⊨ own X2 ∗ own Y1 by the semantics of conditioning modalities. µ′ (E) = Ex∼(X1 )∗ µ′ Eω∼νx [ω ∈ E] = νa1 (E) Let {νx1 ,x2 }x1 ∈JA1 K,x2 ∈JA2 K be a µ′ -disintegration with respect to (X1 , X2 ). By Lemma B.9, {νx1 ,x2 }x2 ∈JA2 K is a νx1 disintegration with respect to X2 for almost all x1 , i.e., {νa1 ,x2 }x2 ∈JA2 K is a µ′ -disintegration with respect to X2 . By applying Lemma B.5 to γ, (D, Y1 ), P ′ ⊨ own X2 ∗ own Y1 , we have (Y1 )∗ νa1 ,a2 = (Y1 )∗ µ′ = (Y1 )∗ νa1 ,a′2 . By Lemma B.6, we have (Y1 )∗ νx1 ,x2 = JM K(x1 , x2 ) for almost all (x1 , x2 ), i.e., for any (x1 , x2 ) ∈ {(a1 , a2 ), (a1 , 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 ∆ = X1 : A1 , . . . , Xn : An be a context, ∆ ⊢ M : GB be an APPL program, and Z ∈ RVJCK be a fresh random variable. Then, we have {own ∆ ∧ own Z} M {Y. C (own Y ∗ own Z)} x̃←∆

where x̃ = (x1 , . . . , xn ) is the tuple of deterministic variables, and we write ∆ to denote both the context and the tuple of random variables (X1 , . . . , Xn ). Proof of Lemma B.10. Let µ be a probability measure on (Ω, ΣΩ ), and D ∈ RVJ∆K be a random variable. Suppose γ, (D, Z), (F, µ|F ) ⊨ own ∆ ∧ own Z. By Lemma B.4, for any Pframe such that Pframe · (F, µ|F ) ⊑ (ΣΩ , µ) and any Dext , there exists µM , Y , and FM such that Pframe · (FM , µM |FM ) ⊑ (ΣΩ , µM ),   ! ω ← µ; ω ← µM ;   , y ← JM K(D(ω));  = ret (Dext (ω), D(ω), Z(ω), Y (ω)) ret (Dext (ω), D(ω), Z(ω), y) and γ, (D, Z, Y ), (FM , µ|FM ) ⊨ own ∆ ∧ own Z ∧ own Y . Now, we show γ, (D, Z, Y ), (FM , µ|FM ) ⊨ Cx̃←∆ (own Y ∗ own Z). By Lemma B.1, it suffices to show that for any µM -disintegration {νx }x∈J∆K with respect to D, for almost all x,

we have Y∗ νx ⊗ Z∗ νx = (Y, Z)∗ νx . Strictly speaking, we need to consider (ΣΩ , µ′M ) ⊒ (FM , µ|FM ) and µ′M -disintegration {νx }x with respect to D, but by Lemma B.3, it suffices to consider µM -disintegration. By Lemma A.6, it suffices to show the following equation for any E, F, G. Ex∼D∗ µM [x ∈ E] · νx (Y −1 (F )) · νx (Z −1 (G)) = Ex∼D∗ µM [x ∈ E] · νx (Y −1 (F ) ∩ Z −1 (G)) This is proved as follows: Ex∼D∗ µM [x ∈ E] · νx (Y −1 (F )) · νx (Z −1 (G)) = Ex∼D∗ µM [x ∈ E] · νx (Y −1 (F )) · Eω∼νx [Z(ω) ∈ G] = Ex∼D∗ µM Eω∼νx [x ∈ E] · νx (Y −1 (F )) · [Z(ω) ∈ G] = Ex∼D∗ µM Eω∼νx [D(ω) ∈ E] · νD(ω) (Y −1 (F )) · [Z(ω) ∈ G] = Eω∼µM [D(ω) ∈ E] · νD(ω) (Y −1 (F )) · [Z(ω) ∈ G] = E(x,z)∼(D,Z)∗ µM [x ∈ E] · νx (Y −1 (F )) · [z ∈ G] = E(x,z)∼(D,Z)∗ µ [x ∈ E] · νx (Y −1 (F )) · [z ∈ G] = E(x,z)∼(D,Z)∗ µ [x ∈ E] · JM K(x)(F ) · [z ∈ G] = E(x,z)∼(D,Z)∗ µ [x ∈ E] · Ey∼JM K(x) [y ∈ F ] · [z ∈ G] = E(x,z)∼(D,Z)∗ µ Ey∼JM K(x) [x ∈ E] · [y ∈ F ] · [z ∈ G] = E(x,z,y)∼(D,Z,Y )∗ µM [x ∈ E] · [y ∈ F ] · [z ∈ G] = Eω∼µM [D(ω) ∈ E] · [Y (ω) ∈ F ] · [Z(ω) ∈ G] = Ex∼D∗ µM Eω∼νx [D(ω) ∈ E] · [ω ∈ Y −1 (F ) ∩ Z −1 (G)] = Ex∼D∗ µM Eω∼νx [x ∈ E] · [ω ∈ Y −1 (F ) ∩ Z −1 (G)] = Ex∼D∗ µM [x ∈ E] · Eω∼νx [ω ∈ Y −1 (F ) ∩ Z −1 (G)] = Ex∼D∗ µM [x ∈ E] · νx (Y −1 (F ) ∩ Z −1 (G)) In Lemma B.10, Z need not be independent of the input variables X1 , . . . , Xn , which makes the lemma stronger than the frame rule H-F RAME. By Lemma B.10, we have the following Hoare triple for the simulator (5): {own X1 ∧ own X2 } Sim(M ) {Y1 . C (own X2 ∗ own Y1 )} x←X1

By (4), this Hoare triple is also satisfied by (Y1 , Y2 ) ← M ; ret Y1 . Thus, we have the desired Hoare triple (3). Precisely speaking, we cannot directly conclude (3) because we have wp(M, X.wp(N, Y.ϕ)) ⊢ wp(X ← M ; N, Y.ϕ) but in general no guarantee for the converse. Proof of Theorem V.1 ( ⇐= ). Suppose that we have γ, D, (Fpre , µpre ) ⊨ own X1 ∧own X2 where γ ∈ J·K and D ∈ RVJX1 : A1 , X2 : A2 K is a random variable. It is straightforward to show that {own(X1 , X2 )} M {(Y1 , Y2 ). own(X1 , X2 , Y1 , Y2 )} holds (Lemma B.4). By unfolding the definition of the Hoare triple, for any Pframe , Dext ∈ RVJ∆ext K, and µ such that Pframe · (Fpre , µpre ) ⊑ (ΣΩ , µ), there exist (DY1 , DY2 ) ∈ RVJY1 : B1 , Y2 : B2 K, µM , and PM such that Pframe · PM ⊑ (ΣΩ , µM ),   ω ← µ;   (y1 , y2 ) ← JM K(D(ω));  ret (Dext (ω), D(ω), y1 , y2 )

ω ← µM ;

ret (Dext (ω), D(ω), DY1 (ω), DY2 (ω))

and γ, (D, DY1 , DY2 ), PM ⊨ own(X1 , X2 , Y1 , Y2 ) hold. Below, we show that the same (DY1 , DY2 ), µM , and PM witness the desired Hoare triple (3). For this purpose, it suffices to show γ, (D, DY1 , DY2 ), PM ⊨ Cx←X1 (own X2 ∗ own Y1 ). By the

D IST-OWN

T RANSFER -OWN

T RANSFER -D IST

E ∼ µ ⊢ own E

own E1 ∧ (E1 = E2 ) ⊢ own E2

E1 ∼ µ ∧ (E1 = E2 ) ⊢ E2 ∼ µ

E Q -C ONGRUENCE

C-E NTAIL

E Q -C ONJ as

own(F [E1 ], F [E2 ]) ∧ (E1 = E2 ) ⊢ F [E1 ] = F [E2 ]

ϕ ∧ (E1 = E2 ) ⊣⊢ ϕ ∗ (E1 = E2 )

ϕ⊢ψ C ϕ⊢ C ψ

x←E

C-S UBST

C-I NDEP

own E ∗ ϕ ⊢ C ϕ x←E

N ECESSITATION

own X ⊢ C (X = x)

⊢ C ϕ

x←E

x←X

FV-OWN

C-O R -S EMI D ISTRIBUTIVE

C (ϕ ∧ ψ) ⊣⊢ C ϕ ∧ C ψ

x←X

Γ; X : K ⊢ E : K E is bijective in X X ∼ unif K ⊢ E ∼ unif K

own E ⊢ C own E

x←X

C-A ND -D ISTRIBUTIVE

⊢ϕ

U NIF -B IJECTION

C-OWN

x←X

C ϕ ∨ C ψ ⊢ C (ϕ ∨ ψ)

x←X

Γ; X1 : A1 , . . . , Xn : An ⊢ E : B own(X1 , . . . , Xn ) ⊢ own E □-M ONO

C-U NIF

own X ∧ C (Y ∼ unif K) ⊢ own X ∗ (Y ∼ unif K) x←X

□-I DEM

□ϕ ⊢ □□ϕ

x←E

□-E LIM

□-T RUE

□ϕ ⊢ ϕ

⊢ □⊤

□-A ND

□ ϕ ∧ □ ψ ⊢ □(ϕ ∧ ψ)

X ∼ µ ∧ (own X ∗ ϕ) ⊢ (X ∼ µ) ∗ ϕ □-C ONJ

ϕ ∧ □ψ ⊢ ϕ ∗ □ψ

ϕ⊢ψ □ϕ ⊢ □ψ

own(X1 , . . . , Xn ) ⊣⊢

n ^

own Xi

i=1

Fig. 12: List of inference rules for Lilac formulas [29]. We omit obvious structural rules like commutativity and associativity of the separating conjunction ∗. Note that Lilac is an affine separation logic, and thus ϕ ∗ ψ ⊢ ϕ holds.

substitution property [29, Lemma B.10], this is equivalent to γ, (D, DY1 ), PM ⊨ Cx←X1 (own X2 ∗ own Y1 ). By Lemma B.10, we have {own X1 ∧ own X2 } Sim(M ) {Y1 . C (own X2 ∗ own Y1 )} x←X1

and thus, there exist DY′ 1 ∈ RVJY1 : B1 K, µSim(M ) , and PSim(M ) such that Pframe · PSim(M ) ⊑ (ΣΩ , µSim(M ) ),   ω ← µ;   y1 ← JSim(M )K(DX1 (ω)); ret (Dext (ω), D(ω), y1 )

ω ← µSim(M ) ;

ret (Dext (ω), D(ω), DY′ 1 (ω))

and γ, (D, DY1 ), PSim(M ) ⊨ Cx←X1 (own X2 ∗ own Y1 ). Here, µM and µSim(M ) are not necessarily the same, but by (4), we have the following equation: ! ! ω ← µSim(M ) ; ω ← µM ; = (10) ret (D(ω), DY′ 1 (ω)) ret (D(ω), DY1 (ω)) The remaining task is to show that if γ, (D, DY′ 1 ), PSim(M ) ⊨ Cx←X1 (own X2 ∗ own Y1 ), then γ, (D, DY1 ), PM ⊨ Cx←X1 (own X2 ∗ own Y1 ). This follows because (D, DY′ 1 )∗ µSim(M ) and (D, DY1 )∗ µM give the same distribution by (10) (see Lemma B.3 for the formal argument). C P ROOFS FOR S ECTION VI (A DDITIONAL P ROOF RULES FOR L ILAC ) A. Proof of Proposition VI.1 Proof of Proposition VI.1 (G EN -W EAK -U NION). Suppose γ, D, P ⊨ ϕ ∗ own(X, Y ). By definition, there exists P1 · P2 ⊑ P such that γ, D, P1 ⊨ ϕ and γ, D, P2 ⊨ own(X, Y ). To show γ, D, P ⊨ Cx:A←X (ϕ ∗ own Y ), suppose P ⊑ (ΣΩ , µ) and let {νx }x∈X be a µ-disintegration with respect to X. By the proof of C-I NDEP, we know that νx |P1 = P1 for almost all x. We also have γ, D, νx |P2 ⊨ own(X, Y ) because own(X, Y ) does not depend on the probability distribution. Thus, it suffices to

show that νx |P1 · νx |P2 ⊑ νx holds for almost all x. Since we already know that P1 · P2 ⊑ P, we show that for almost all x, for any F ∈ FP1 and G ∈ FP2 , νx (F ∩ G) = νx (F )νx (G). By Lemma A.6, this is equivalent to Ex∼(X(γ)◦D)∗ µ [x ∈ E] · νx (F ∩ G) = Ex∼(X(γ)◦D)∗ µ [x ∈ E] · νx (F ) · νx (G) which is proved as follows. Ex∼(X(γ)◦D)∗ µ [x ∈ E] · νx (F ) · νx (G) = Ex∼(X(γ)◦D)∗ µ [x ∈ E] · µ(F ) · νx (G) = µ(F )Ex∼(X(γ)◦D)∗ µ [x ∈ E] · Eω∼νx [ω ∈ G] = µ(F )Ex∼(X(γ)◦D)∗ µ Eω∼νx [ω ∈ G ∩ (X(γ) ◦ D)−1 (E)] = µ(F )Eω∼µ [ω ∈ G ∩ (X(γ) ◦ D)−1 (E)] = µ(F )µ(G ∩ (X(γ) ◦ D)−1 (E)) = µ(F ∩ G ∩ (X(γ) ◦ D)−1 (E)) by γ, D, P2 ⊨ own X and P1 · P2 ⊑ (ΣΩ , µ) = Ex∼(X(γ)◦D)∗ µ Eω∼νx [ω ∈ F ∩ G ∩ (X(γ) ◦ D)−1 (E)] = Ex∼(X(γ)◦D)∗ µ Eω∼νx [ω ∈ F ∩ G] · [x ∈ E] = Ex∼(X(γ)◦D)∗ µ [x ∈ E] · νx (F ∩ G) Proof of Proposition VI.1 (C ONTRACTION). Suppose γ, D, P ⊨ (own W ∗ own X) ∧ Cx←X (own W ∗ own Y ). Let FX and FW be the sub-σ-algebras generated by X and W , respectively. Let µ be a probability measure on (Ω, ΣΩ ) such that P ⊑ (ΣΩ , µ). By γ, D, P ⊨ own W ∗ own X, we have (µ|FX , FX ) · (µ|FW , FW ) ⊑ (µ, ΣΩ ). By γ, D, P ⊨ Cx←X (own W ∗ own Y ), for any µ-disintegration {νx }x∈X with respect to X, there exists FY ⊆ F such that Y is FY -measurable and (νx |FW , FW ) · (νx |FY , FY ) ⊑ (νx , ΣΩ ) for almost all x. By the proof of C-I NDEP, we know that νx |FW = µ|FW for almost all x. Now, we show that for any E1 ∈ FX , E2 ∈ FY , and E3 ∈ FW , we have µ(E1 ∩ E2 ∩ E3 ) = µ(E1 ∩ E2 ) · µ(E3 ). Since FX = {X −1 (E) | E ∈ ΣX }, there exists EX ∈ ΣX such that E1 = X −1 (EX ). µ(E1 ∩ E2 ∩ E3 ) = Ex∼X∗ µ Eω∼νx [ω ∈ X −1 (EX )] · [ω ∈ E2 ∩ E3 ] = Ex∼X∗ µ [x ∈ EX ] · Eω∼νx [ω ∈ E2 ∩ E3 ] = Ex∼X∗ µ [x ∈ EX ] · νx (E2 ) · νx (E3 ) = Ex∼X∗ µ [x ∈ EX ] · νx (E2 ) · µ(E3 ) = Ex∼X∗ µ [x ∈ EX ] · νx (E2 ) · µ(E3 ) = Ex∼X∗ µ Eω∼νx [ω ∈ X −1 (EX )] · [ω ∈ E2 ] · µ(E3 ) = µ(E1 ∩ E2 ) · µ(E3 ) Consider the following set. {E ∈ σ(FX ∪ FY ) | ∀E3 ∈ FW , µ(E ∩ E3 ) = µ(E) · µ(E3 )} It is easy to see that this is a λ-system containing the π-system {E1 ∩E2 | E1 ∈ FX , E2 ∈ FY }. By Dynkin’s π-λ theorem, the λ-system contains σ({E1 ∩ E2 | E1 ∈ FX , E2 ∈ FY }) = σ(FX ∪ FY ). Hence, we have (µ|FX , FX ) · (µ|σ(FX ∪FY ) , σ(FX ∪ FY )) ⊑ (µ, ΣΩ ). Note that σ(FX ∪ FY ) is countably generated because both FX and FY are countably generated. B. Generalized U NIF -B IJECTION Lemma C.1. U NIF -B IJECTION can be generalized to the following. Γ; ∆, Y : K ⊢ E : K E is bijective in Y own ∆ ∗ F ∼ unif K ⊢ own ∆ ∗ E[F/Y ] ∼ unif K Proof sketch. Suppose that we have own ∆ ∗ F ∼ unif K. By C-I NDEP, we have Cx←∆ (F ∼ unif K). By C-S UBST, we as have Cx←∆ (E[x/∆] = E ∧ F ∼ unif K). By applying U NIF -B IJECTION to E[x/∆], we have Cx←∆ (E[F/Y ] ∼ unif K). Finally, by C-U NIF, we have own ∆ ∗ E[F/Y ] ∼ unif K.

C. Proof of Lemma VI.5 Proof of Lemma VI.5. Without loss of generality, we show the case where ∆ = {W1 , W2 }, X = {X1 , X2 }, and Y = {Y1 , Y2 }. Also, let I = {W1 }, OM = {X1 }, and ON = {Y1 }. Then, we have the following. W2 ⊥ X1 | W1 ∧ W2 , X2 ⊥ Y1 | W1 , X1 =⇒ W2 ⊥ X1 | W1 ∧ W2 ⊥ Y1 | W1 , X1 =⇒ W2 ⊥ X1 , Y1 | W1 =⇒ W2 ⊥ Y1 | W1 D P ROOFS FOR S ECTION VII (A PPLICATIONS TO P ROBING S ECURITY ) A. Detailed Proof of Theorem VII.1 Proof of Theorem VII.1. The proof outline is shown in Fig. 7. Here, we show non-trivial entailments used in the proof. We often use E Q -C ONJ implicitly in the following. ′ as j j ′ • X = X[V + ρj /X ] ∗ I(j; X) ⊢ I(j + 1; X ): By definition of I(j; X), the premise is equivalent to as

∗ X =V +ρ . k as

X′ = X[V j + ρj /X j ] ∗ own(V, ρ, X) ∗

k<j k

– For each k ̸= j, we have own X ′ by T RANSFER -OWN. k as

X ′ = X k ∧ own X j ⊢ own X ′

– We have own X ′ by T RANSFER -OWN and FV-OWN. k as

own V k ∧ own ρj ∧ X ′ = V k + ρj k as

⊢ own(V k + ρj ) ∧ X ′ = V k + ρj ⊢ own X ′

k as

– For each k < j, we have X ′ = V k + ρk by transitivity of =. as

k as

X k = V k + ρk ∧ X ′ = X k ⊢ X ′ = V k + ρk j as

– We immediately have X ′ = V j + ρj from the premise. Therefore, we obtain the following entailments.

∗

X k = V k + ρk X′ = X[V j + ρj /X j ] ∗ own(V, ρ, X) ∗ k<j ^ k as j as ⊢ own(V, ρ) ∧ own X′ ∧ (X ′ = V k + ρk ) ∧ X ′ = V j + ρj k<j

⊢ I(j + 1; X′ ) •

I(t + 1; X) ⊢ C(v,r)←(V∩I,ρ∩I) (own(V \ I, ρ \ I) ∗ own O): as

own(V, ρ) ∗ X = V + ρ ⊢

C (v,r)←(V∩I,ρ∩I)

∧

(own(V, ρ) ∗ X = V + ρ) ^ as as (v j = V j ∧ rj = ρj ) C

(v,r)←(V∩I,ρ∩I)

⊢

by C-S UBST

X j ∈O as

((own(V, ρ) ∗ X = V + ρ) ∧

by G EN -W EAK -U NION

(v,r)←(V∩I,ρ∩I)

(v j = V j ∧ rj = ρj ))

by C-A ND -D ISTRIBUTIVE

X j ∈O

– By FV-OWN and □-M ONO and □-T RUE, we have ⊢ □ own(v j + rj ) for each X j ∈ O. – For each X j ∈ O, we also have the following entailment. as

own V j ∧ own ρj ∧ v j = V j ∧ rj = ρj as

⊢ own(v j + rj , V j + ρj ) ∧ v j = V j ∧ rj = ρj j

⊢ v + rj = V + ρ j

by FV-OWN E Q -C ONGRUENCE

Thus, we continue as follows. as

((own(V, ρ) ∗ X = V + ρ) ∧

(v,r)←(V∩I,ρ∩I)

⊢

X j ∈O as

(v,r)←(V∩I,ρ∩I)

⊢

(v,r)←(V∩I,ρ∩I)

⊢

by transitivity

(□ own(v j + rj ) ∧ v j + rj = X j ))

by □-C ONJ

X j ∈O

(own(V \ I, ρ \ I) ∗

(□ own(v j + rj ) ∧ v j + rj = X j ))

X j ∈O

(own(V \ I, ρ \ I) ∗

(□ own(v j + rj ) ∧ v j + rj = V j + ρj ))

X j ∈O

(own(V \ I, ρ \ I) ∧

⊢

(own(V \ I, ρ \ I) ∧ X = V + ρ ∧

⊢

(v j = V j ∧ rj = ρj ))

(own(v j + rj ) ∧ v j + rj = X j ))

by □-E LIM

X j ∈O

(own(V \ I, ρ \ I) ∗ own O)

by T RANSFER -OWN

(v,r)←(V∩I,ρ∩I)

B. Detailed Proof of Theorem VII.4 Proof of Theorem VII.4. The outline of the proof is shown in Fig. 9. We show the non-trivial entailments used in the proof. We often use E Q -C ONJ implicitly in the following. j j ′′ ′′ as i i ′′ ′′ • S ∼ unif K∗(C , R ) = (C, R)[Cj−1 +S/Cj , Ci −S/Ci+1 , S/Ri,j ]∗I(i, j; C, R) ⊢ I(i, j+1; C , R ): by T RANSFER i D IST and E Q -C ONGRUENCE. Note that fj is defined so that the following holds for each i, j such that i < j. j fi+1 (R) = fij (R) − Ri,j

i fji (R) = fj−1 (R) + Ri,j , •

∗ (R ∼ unif K) ∗ ∗ (C = A + f (R)) ⊢ C (own(A \ I) ∗ own O): It suffices to prove the own A ∗ ∗ (R ∼ unif K) ⊢ C (own(A \ I) ∗ ϕ ) (11)

own A ∗ following.

i,j

i<j

i as j

i,j

i j

a←I

i,j

O own

a←I

i<j

where ^

ϕO own :=

own Ri,j ∧

Ri,j ∈O

own(ai + fji (R)) ∧

Cji ∈O,j<t

own(Ai + fti (R))

Cti ∈O

because we have the following entailments then.

∗ (R ∼ unif K) ∗ ∗(C = A + f (R)) ^ ⊢ C (own(A \ I) ∗ ϕ ) ∧ own I ∗ ∗(C = A + f (R)) ∧ C (a = A ) ^ ⊢ C (own(A \ I) ∗ ϕ ) ∧ C ∗(C = A + f (R)) ∧ C (a = A ) ^ (a = A )) ⊢ C ((own(A \ I) ∗ ϕ ) ∧ ∗(C = A + f (R)) ∧

own A ∗

i as j

i,j

i<j

i,j

O own

a←I

O own

a←I

O own

a←I

⊢ C (own(A \ I) ∗ a←I

^ Ri,j ∈O

∧

i j

i,j

a←I i,j

i,j

i as j

own Ri,j ∧

i as j

i as

i j

by C-S UBST

a←I

Ai ∈I i as i

i j

by C-I NDEP

a←I

Ai ∈I i as i

i j

by C-A ND -D ISTRIBUTIVE

Ai ∈I

(own(ai + fji (R)) ∧ Cji = ai + fji (R))

Cji ∈O,j<t

as (own(Ai + fti (R)) ∧ Cji = Ai + fji (R)) )

Cti ∈O

⊢ C (own(A \ I) ∗ own O)

by T RANSFER -OWN

a←I

Now, we prove (11). Observe that free variables in fji (R) are the first j elements of R0,i , R1,i , . . . , Ri−1,i , Ri,i+1 , Ri,i+2 , . . . , Ri,t Let S ⊆ R be the set of random variables defined as follows. S := {Ri,j | Ri,j ∈ O ∨ Ri,j is a free variable in fji (R) for some Cji ∈ O such that j < t}

(12)

Then, the intersection of S and (12) is a subset of {Ri,j | i < j ∧ Aj ∈ I} ∪ {Rj,i | j < i ∧ Aj ∈ I}, which has at most |I| elements. Since |I| + |{Cji ∈ O | j = t}| ≤ |O| ≤ t, there exists an injective mapping from Cti ∈ O to Rj,k ∈ R \ S such that j = i or k = i (i.e., random variables in (12) excluding those in S). We write such Rj,k as R[Cti ]. Then, for each Cti ∈ O, we can see that Ai + fti (R) is a bijective function of R[Cti ] when other variables are fixed. Thus, we have the following entailments. own A ∗

∗ (R ∼ unif K) i,j

i<j

⊢ C

own A ∗

a←I

⊢ C

∗ (R ∼ unif K)

by G EN -W EAK -U NION

i,j

i<j

∗

own(A \ I) ∗

a←I

⊢ C

Cti ∈O

own(A \ I) ∗

a←I

(R[Cti ] ∼ unif K) ∗

∗ (A

Cti ∈O

∗ (R ∼ unif K)

i,j

Ri,j ∈S

+ fti (R) ∼ unif K) ∗

∗ (R ∼ unif K)

! by Lemma C.1

i,j

Ri,j ∈S

V V Moreover, since expressions in Ri,j ∈O own Ri,j ∧ C i ∈O,j<t own(ai + fji (R)) contain only random variables in S and j deterministic variables, we have the following entailments.

∗ (R ∼ unif K) i,j

Ri,j ∈S

⊢ own S ^ ⊢ own Ri,j ∧ Ri,j ∈O

by D IST-OWN ^

own(ai + fji (R))

by FV-OWN

Cji ∈O,j<t

C. Proof of Theorem VII.8 Lemma D.1. Let E be a deterministic expression such that Γ; · ⊢ E : A. Then, we have as

X=E

⊢

own X

Proof. as

X=E as

⊢ X = E ∧ own E

by FV-OWN

⊢ own X

by T RANSFER -OWN

Lemma D.2. Let Γ; ∆, X : A ⊢ E : B be an expression. Then, we have (own ∆ ∧ own X) ∗ ϕ

⊢

as (own ∆ ∧ own X) ∗ ϕ ∗ E = E[x/X]

x←X

Proof. (own ∆ ∧ own X) ∗ ϕ ⊢ C

x←X

⊢ C

as (own ∆ ∧ own X) ∗ ϕ ∧ C X = x x←X as (own ∆ ∧ own X) ∗ ϕ ∧ X = x

by G EN -W EAK -U NION and C-S UBST by C-A ND -D ISTRIBUTIVE

x←X

as ⊢ C (own ∆ ∧ own X) ∗ ϕ ∧ own(E, E[x/X]) ∧ X = x x←X as ⊢ C (own ∆ ∧ own X) ∗ ϕ ∧ E = E[x/X] x←X as ⊢ C (own ∆ ∧ own X) ∗ ϕ ∗ E = E[x/X] x←X

Proof of Theorem VII.8. I, J, KQ , and KS satisfy the following conditions: 1) |I|, |J| ≤ |O \ Ct | 2) If Cji ∈ O and j < t, then i ∈ I ∩ J. 3) If i < j, Cji ∈ O, and i < k ≤ j < t, then (i, k) ∈ KQ . 4) If Cji ∈ O, k < i, j < t, and (k, i) ∈ KQ , then k, i ∈ I and k, i ∈ J. 5) If Qi,j ∈ O, then (i, j) ∈ KQ .

by FV-OWN by E Q -C ONGRUENCE by E Q -C ONJ

6) If Ri,j ∈ O, then (i, j) ∈ KQ , i ∈ I, and j ∈ J. 7) If (i, j) ∈ KQ and Si,j ∈ O, then i, j ∈ I and i, j ∈ J. 8) If Cti ∈ O and there exists j < t with Cji ∈ O, then Vi ⊆ KQ ∪ KS . 9) If Cti ∈ O and there is no j < t with Cji ∈ O, then Vi \ (KQ ∪ KS ) ̸= ∅. Here, Vi = {(k, i) | k < i} ∪ {(i, k) | i < k} is the indices of the free variables in gti (Q, S). Condition 9 follows because |Vi ∩ (KQ ∪ KS )| ≤ |O \ Ct | < |Vi | = t. Vi ∩ (KQ ∪ KS ) = Vi ∩ {(i, j) | Qi,j ∈ Q ∨ Ri,j ∈ O ∨ Si,j ∈ O} ∪ {(k, i) | k < i, Cjk ∈ O, j < t} ∪ {(i, k) | i < k, Cjk ∈ O, j < t} In other words, we have |O ∩ Ct | ≤ |Vi \ (KQ ∪ KS )|. Thus, for each Cti ∈ O with no j < t such that Cji ∈ O, we take an element of Vi \ (KQ ∪ KS ) in such a way that the chosen elements are distinct for distinct Cti ’s, and define the set KC as the set of the chosen elements. By applying the rules in Fig. 4, we obtain the following postcondition (Fig. 11). own(A, B) ∗

∗ P = A × B ∗ ∗ Q ∼ unif K ∗ ∗ R = Q + P ∗ ∗ S = R + P ∗ ∗ C = P + g (Q, S) as

i,j

i<j

i,j

i<j

i,j

j,i

i<j

i,j

i as j

i,i

i j

By applying G EN -W EAK -U NION and C-S UBST, we have the following postcondition. C

∗ P = A × B ∗ ∗ Q ∼ unif K ∗ ∗ R = Q + P ∗ ∗ S = R + P ∗ ∗ C = P + g (Q, S) ∗ ∗ A = a ∗ ∗ B = b as

own(A, B) ∗

(a,b)←(I,J )

i,j

i as j

i,i

i,j

i j

i,j

i<j

i∈I

i,j

i<j

i,j

j,i

i<j

j∈J

It follows that the above postcondition implies: ^ ^ as as own(A, B) ∗ Qi,j ∼ unif K ∧ own(A, B, Q) ∧ Pi,j = Ai × B j ∧ Ri,j = Qi,j + Pi,j C

∗

(a,b)←(I,J )

∧

i<j

i,j

Si,j = Ri,j + Pj,i ∧

i<j

Cji = Pi,i + gji (Q, S) ∧

i,j

i<j

Ai = ai ∧

i∈I

as B j = bj

j∈J

Then, we focus on the underlined part; rewrite the equations for Pi,j , Ri,j , Si,j , and Cji ; and obtain equations for O. • Pi,j : ^ ^ ^ as as as Pi,j = Ai × B j ∧ Ai = ai ∧ B j = bj i,j

i∈I as

⊢

Pi,j = a × b

j∈J j

(i,j)∈I×J as

⊢

Pi,j = ai × bj

Pi,j ∈O •

Ri,j : own Q ∧

i<j

⊢

Pi,j = ai × bj

(i,j)∈I×J as

Ri,j = Qi,j + Pi,j ∧ i

Ri,j = Qi,j + a × b

Ri,j ∈O

•

Si,j : own(A, B, Q) ∧

i,j

⊢

^ i<j

Pi,j = Ai × B j ∧

i<j i

Si,j = Qi,j + A × B + A × B

Ri,j = Qi,j + Pi,j ∧

^ i<j

Si,j = Ri,j + Pj,i

If Si,j ∈ O and (i, j) ∈ KQ , then i, j ∈ I and i, j ∈ J by Condition 7, and thus: ^ ^ ^ as as as Si,j = Qi,j + Ai × B j + Aj × B i ∧ Ai = ai ∧ B j = bj i<j

i∈I as

⊢

j∈J

Si,j = Qi,j + a × b + a × b

(i,j)∈KQ ,Si,j ∈O •

Cji : First note that we have Cji = Ai × B i + gji (Q, S) from Cji = Pi,i + gji (Q, S) and Pi,i = Ai × B i . – If Cji ∈ O and j < t, then i ∈ I and i ∈ J by Condition 2. ^ ^ ^ ^ as as as as own(A, B, Q) ∧ Cji = Ai × B i + gji (Q, S) ∧ Si,j = Qi,j + Ai × B j + Aj × B i ∧ Ai = ai ∧ B j = bj i,j

⊢

i<j

i∈I

j∈J

as Cji = ai × bi + gji (Q, S)

^ Cji ∈O,j<t

If Sk,i is a free variable in gji (Q, S) and (k, i) ∈ KQ , then by Condition 4, k, i ∈ I and k, i ∈ J, and thus as Sk,i = Qk,i + ak × bi + ai × bk . Hence, we obtain ^ as Cji = ai × bi + hij (Q, S) Cji ∈O,j<t

where hij (Q, S) is defined as follows. X X  (Qk,i + ak × bi + ai × bk ) + Sk,i    k<j,(k,i)∈KQ k<j,(k,i)∈K / Q i X X X hj (Q, S) :=  (Qk,i + ak × bi + ai × bk ) + Sk,i + Qi,k   k<i,(k,i)∈K / Q

k<i,(k,i)∈KQ

i≥j i<j

i<k≤j

Note that the free variables in hij (Q, S) are in {Si,j | (i, j) ∈ KS \ KQ } ∪ {Qi,j | (i, j) ∈ KQ } if Cji ∈ O and j < t. – If Cti ∈ O and there exists j < t with Cji ∈ O, then similarly to the previous case, we have the following equations. ^ as Cti = ai × bi + hit (Q, S) Cti ∈O,(∃j<t,Cji ∈O)

The free variables in hit (Q, S) are in {Si,j | (i, j) ∈ KS \ KQ } ∪ {Qi,j | (i, j) ∈ KQ }. – If Cti ∈ O and there exists no j < t with Cji ∈ O: ^ ^ as as own(A, B, Q) ∧ Cji = Ai × B i + gji (Q, S) ∧ Si,j = Qi,j + Ai × B j + Aj × B i i,j

i<j as Cti = Ai × B i + gti (Q, {Qi,j + Ai × B j + Aj × B i }i<j )

⊢

Cti ∈O,¬(∃j<t,Cji ∈O)

Note that for each such Cti , there exists Qi′ ,j ′ ∈ KC that occurs in gti (Q, {Qi,j + Ai × B j + Aj × B i }i<j ), and moreover, the right-hand side of the above equation is a bijective expression in Qi′ ,j ′ . By E Q -C ONJ, we now have the following postcondition. as own(A, B) ∗ Qi,j ∼ unif K ∗ Si,j = Qi,j + Ai × B j + Aj × B i C

∗

(a,b)←(I,J )

∗

Ri,j = Qi,j + ai × bj ∧

Ri,j ∈O as Cji = ai × bi + hij (Q, S) ∧

Cji ∈O,j<t

∗

(i,j)∈KS \KQ

Pi,j = ai × bj ∧

Pi,j ∈O

∧

∗

i<j

Cti ∈O,¬(∃j<t,Cji ∈O)

Si,j = Qi,j + ai × bj + aj × bi

(i,j)∈KQ ,Si,j ∈O

as Cti = ai × bi + hit (Q, S)

Cti ∈O,(∃j<t,Cji ∈O)

as Cti = Ai × B i + gti (Q, {Qi,j + Ai × B j + Aj × B i }i<j )

Now, we divide

∗

i<j Qi,j ∼ unif K into three parts (technically, four parts, but one part is discarded).

∗ Q ∼ unif K ⊢ ∗ Q ∼ unif K ∗ ∗ i,j

i<j

i,j

(i,j)∈KS \KQ

(i,j)∈KQ

∗

Qi,j ∼ unif K ∗

Qi,j ∼ unif K

(i,j)∈KC

Then, we apply Lemma C.1 and T RANSFER -U NIFORM to the second part and the third part, respectively.

∗

own(A, B) ∗

(i,j)∈KS \KQ

Qi,j ∼ unif K ∗

∗

⊢ own(A, B) ∗

(i,j)∈KS \KQ

own(A, B) ∗

∗

Si,j = Qi,j + Ai × B j + Aj × B i

Si,j ∼ unif K

Qi,j ∼ unif K ∗

(i,j)∈KC

∗

⊢ own(A, B) ∗

∗

(i,j)∈KS \KQ

Cti ∈O,¬(∃j<t,Cji ∈O)

∗

Cti ∈O,¬(∃j<t,Cji ∈O)

Cti ∼ unif K

The current postcondition is as follows. own(A, B) ∗ Qi,j ∼ unif K ∗ C

∗

(a,b)←(I,J )

∗

(i,j)∈KQ

Pi,j = ai × bj ∧

Pi,j ∈O

∧

∗

(i,j)∈KS \KQ

Si,j ∼ unif K

Ri,j ∈O

Si,j = Qi,j + ai × bj + aj × bi

(i,j)∈KQ ,Si,j ∈O

as Cji = ai × bi + hij (Q, S) ∧

∗

Ri,j = Qi,j + ai × bj ∧

Cji ∈O,j<t

∗

Cti = Ai × B i + gti (Q, {Qi,j + Ai × B j + Aj × B i }i<j )

as Cti = ai × bi + hit (Q, S)

^ Cti ∈O,(∃j<t,Cji ∈O)

Cti ∈O,¬(∃j<t,Cji ∈O)

Cti ∼ unif K

Here, the free variables of the right-hand sides of the remaining equations are in {Qi,j | (i, j) ∈ KQ }∪{Si,j | (i, j) ∈ KS \KQ }. By applying T RANSFER -OWN, we obtain the following postcondition. ^ ^ ^ ^ own(A, B) ∗ own Qi,j ∧ own Si,j ∧ own Pi,j ∧ own Ri,j C (a,b)←(I,J )

∧

(i,j)∈KQ ,Si,j ∈O

own Si,j ∧

Pi,j ∈O

(i,j)∈KS \KQ

(i,j)∈KQ

own Cji ∧

Cji ∈O,j<t

own Cti

Cti ∈O,(∃j<t,Cji ∈O)

By definition of KQ and KS , we finally have the following postcondition. C (a,b)←(I,J )

(own(A \ I, B \ J ) ∗ own O)

Ri,j ∈O

∗

Cti ∈O,¬(∃j<t,Cji ∈O)

Cti ∼ unif K

Record · ID 222550 · SHA-256 c640b98fa404c2cb
Retrieved via Conceptio — every document is proof-bundled with source, license, and retrieval metadata.