💻 computer science

Formal Verification of Probing Security via Conditional Independence

This paper proposes a novel formal verification approach for the probing security of masked cryptographic algorithms by leveraging probabilistic separation logic (Lilac) to establish a connection between noninterference properties and conditional independence.

Original authors: Satoshi Kura, Katsuyuki Takashima

Published 2026-05-25

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Satoshi Kura, Katsuyuki Takashima

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to keep a secret recipe safe in a busy, noisy kitchen. In the world of cryptography, this "secret recipe" is a private key, and the "noise" is a side-channel attack. Attackers aren't trying to break the math; they are trying to peek at the "leaks" (like power usage or timing) while the computer is crunching numbers to guess your secret.

To stop this, cryptographers use a technique called Masking. Think of masking like shredding your secret recipe into $t+1$ pieces of paper (shares). You give one piece to each of $t+1$ different chefs. As long as an eavesdropper can only peek at $t$ pieces (or fewer), they see nothing but random gibberish. They can't reconstruct the recipe because they are missing at least one crucial piece.

However, proving that a complex recipe (algorithm) is truly safe is incredibly hard. If you try to check it by hand, you might miss a tiny leak, and the whole security system fails. This is where the paper comes in.

The Problem: Checking the "Leak"

The authors want to build a formal proof (a mathematical guarantee) that a masked algorithm is safe. Traditionally, this is done using a "Simulator" concept.

The Simulator Idea: Imagine a magic box (the simulator) that tries to recreate exactly what the eavesdropper sees. If the magic box can create the exact same "leak" using only the public information (like the ingredients list) and without ever seeing the secret recipe pieces, then the real algorithm is safe. The eavesdropper learns nothing new.

But building these simulators by hand is error-prone. The authors wanted a better way to prove this.

The Solution: A New Logic Tool (Lilac)

The authors introduce a connection between "Simulators" and a concept called Conditional Independence.

The Analogy: Imagine you are trying to guess a friend's birthday (the secret).
- Scenario A: You know their age and the month they were born (Public Info).
- Scenario B: You also know their secret diary entry (Secret Info).
- Conditional Independence: If knowing the diary entry doesn't change your guess about the birthday once you already know the age and month, then the diary is "conditionally independent" of the birthday given the age/month.

The paper proves that if a simulator exists, then the secret is conditionally independent of the leak, given the public info.

To check this mathematically, they use a tool called Lilac.

What is Lilac? Think of Lilac as a very strict, super-powered rulebook for probability. It's like a logic game where you have to prove that two piles of cards (random variables) are shuffled independently of each other.
The "Separating Conjunction": In this rulebook, there is a special symbol (like a magic wand) that says, "These two piles of cards are totally separate and don't influence each other."
The Innovation: The authors added new rules to this rulebook to handle "Conditioning" (the "given that..." part). This allows them to prove that even if the eavesdropper sees some data, it doesn't reveal the secret because they already have the public data.

What They Actually Did

The authors didn't just talk about theory; they built a system to verify real cryptographic algorithms using this new logic. They applied their method to three specific "gadgets" (building blocks) used in modern encryption:

MINIADDREPNOISE: A tool used to add random noise to data (like adding salt to a soup to hide the original flavor). They proved that even if an attacker peeks at some of the salted soup, they can't figure out the original flavor.
REFRESH: A tool that takes the shredded pieces of the secret and re-shuffles them so they look brand new, preventing attackers from tracking them over time. They proved this re-shuffling is safe.
SECMULT (Secure Multiplication): A tool that multiplies two secret numbers together without revealing the result until the very end. This is one of the hardest operations to secure. They proved this multiplication is safe against the "t-probing" attacks.

The Bottom Line

The paper claims that by translating the complex idea of "Simulators" into the language of "Conditional Independence," they can use the Lilac logic system to automatically and rigorously verify that these cryptographic tools are safe.

They successfully demonstrated this by writing formal proofs for MINIADDREPNOISE, REFRESH, and SECMULT, showing that these specific algorithms satisfy the strict security requirements needed to protect secrets against side-channel attacks. They did not claim to fix all future security problems or apply this to medical devices; their work is strictly about proving the safety of these specific cryptographic math operations using a new logical framework.

Technical Summary: Formal Verification of Probing Security via Conditional Independence

Problem Statement

Side-channel attacks pose a significant threat to the security of cryptographic schemes, prompting the widespread adoption of masking as a countermeasure. Masking splits secret values into shares to ensure that leakage from any subset of intermediate values does not reveal the underlying secret. However, proving the security of masked algorithms, particularly under the ISW probing model (where an adversary can probe up to $t$ intermediate values), is notoriously error-prone when done manually. Several flaws have been identified in manual security proofs, necessitating formal verification.

While probabilistic separation logic has been successfully applied to verify properties like input independence (e.g., in one-time pads), it has not yet been utilized to verify probing security (specifically $t$ -noninterference) of masked algorithms. Existing formal verification tools often rely on substitution-based methods or type inference, which may lack the modularity or expressiveness required for complex conditional independence reasoning inherent in masking.

Methodology

This work proposes a novel approach to formal verification by establishing a rigorous connection between simulator-based security definitions and conditional independence. The methodology relies on Lilac, a probabilistic separation logic designed to reason about conditional independence.

1. Theoretical Foundation: Simulators and Conditional Independence

The authors rephrase the standard simulator-based definition of noninterference in terms of conditional independence.

Simulator-based view: A masked algorithm is secure if, for any set of probes $O$ (observed by an adversary), there exists a simulator that can generate the distribution of $O$ using only a subset of input shares $I$ , without access to the remaining secret shares.
Conditional independence view: This security requirement is equivalent to the statement that the observed values $O$ are conditionally independent of the secret input shares ( $\Delta \setminus I$ ) given the public input shares $I$ . Formally, this is expressed as $O \perp (\Delta \setminus I) \mid I$ .

The paper demonstrates that this equivalence holds within the semantic framework of Lilac, which models probabilistic independence using independent combinations of probability spaces and conditioning via disintegration.

2. Extension of Lilac

To apply Lilac to probing security, the authors extend the logic with specific proof rules that were not present in the original Lilac formulation:

Semi-Graphoid Axioms: The paper proves that the semi-graphoid axioms for conditional independence (Symmetry, Decomposition, Weak Union, and Contraction) hold within Lilac's semantics. These axioms are crucial for manipulating conditional independence statements during proofs.
Composability Rules: New rules are introduced to handle the composition of noninterference properties, specifically for sequential composition and for-loops. These rules allow for modular verification of complex algorithms built from smaller gadgets.
Ownership and Weakening: Additional rules facilitate reasoning about ownership of random variables and the weakening of noninterference properties when dealing with unshared inputs or subsets of variables.

3. Verification Framework

The verification process involves:

Translating masked algorithms (written in the probabilistic programming language APPL) into Hoare triples within Lilac.
Using the established equivalence (Theorem V.1) to reduce the verification of $(I, O)$ -noninterference to proving a specific conditional independence Hoare triple:
$\{ \text{own } \Delta \} \ M \ \{ Y. \ C_{x \leftarrow I}(\text{own}(\Delta \setminus I) * \text{own } O) \}$
Applying the extended set of proof rules (including the new semi-graphoid and composability rules) to derive the required entailments.

Key Contributions

Formal Connection: The paper establishes a formal equivalence between simulator-based definitions of probing security and conditional independence properties expressible in Lilac. This bridges the gap between cryptographic security notions and probabilistic separation logic.
Extension of Lilac: The authors provide a suite of additional proof rules necessary for verifying masked algorithms, including the semi-graphoid axioms for conditional independence and composability rules for sequential composition and loops.
Case Studies: The effectiveness of the approach is demonstrated by formally verifying the probing security of three critical algorithms using Lilac:
- MINIADDREPNOISE: A subroutine for adding uniform noise to masked values.
- REFRESH: A fundamental algorithm for refreshing shares to prevent leakage accumulation.
- SECMULT: A standard masked multiplication algorithm.
- ADDREPNOISEER: A variant used in the Raccoon signature scheme (a candidate for NIST Post-Quantum Cryptography standardization), proving it satisfies the $t$ -Strong Noninterference with Unshared Input ( $t$ -SNIU) property.

Results

The paper successfully derives Hoare triples for the target algorithms, confirming their noninterference properties.

For MINIADDREPNOISE, the proof shows that the output shares are conditionally independent of the unobserved input shares given the observed inputs.
For REFRESH, the proof verifies that the algorithm satisfies $t$ -Strong Noninterference ( $t$ -SNI), a stronger property than standard noninterference, which is essential for composability in higher-order masking.
For SECMULT and ADDREPNOISEER, the proofs leverage the new composability rules to handle the nested loops and complex data dependencies inherent in these algorithms.

The verification of ADDREPNOISEER is particularly significant as it validates a key component of the Raccoon signature scheme's security proof, which relies on the $t$ -SNIU property.

Significance and Claims

The authors claim that this work provides the first application of probabilistic separation logic (specifically Lilac) to the formal verification of probing security for masked algorithms. By translating security proofs into conditional independence reasoning, the approach offers a modular and logically rigorous alternative to existing substitution-based or type-inference tools.

The paper emphasizes that while the underlying idea of connecting simulators to conditional independence is conceptually simple, its formalization in Lilac is technically non-trivial due to the logic's reliance on independent combinations rather than standard product probability spaces. The successful derivation of the main theorem and the application to real-world cryptographic components (Raccoon) demonstrate that this framework is viable for verifying complex, high-order masking schemes.

The work remains modest regarding its scope, noting that the current results are limited to the information-theoretic setting of probing security. The authors identify extending the approach to the computational setting and implementing the method in an interactive theorem prover as important directions for future work. They also suggest that the framework could be applied to other simulator-based security properties, such as those found in secure multi-party computation.