← All papers
First page of Leakage-Resilient Computation via Matrix Refreshing

Leakage-Resilient Computation via Matrix Refreshing

Stefan Dziembowski, Sebastian Faust

cs.CR Nov 3, 2026 · v1
Formalizes the continual matrix-refreshing security bound, NAND circuit compiler composition theorem, and expected-work simulator in Lean 4 with Mathlib, checked via Lean comparator.
Leakage-resilient cryptography protects secrets against side-channel attacks, in which a physical implementation reveals partial information about its internal state. A fundamental primitive in this area is a leakage-resilient storage, which allows a secret to be stored in a way that remains secure even if an adversary learns some information about the storage's internal state. A popular approach represents a secret as the inner product of two $n$-bit vectors, called shares. The shares are stored and processed separately by two parts of the implementation, called the left and right parties. Because leakage accumulates over time, the shares must be refreshed repeatedly. We prove that a simple refresh, in which the left party multiplies its share by a uniform invertible matrix $M$ and the right party multiplies its share by $M^{-1}$, is secure under continual local leakage. After $T$ refreshes, each allowing at most $λ$ bits of leakage per party, the transcripts for two stored secrets are at statistical distance at most $C\cdot T\cdot 2^{6λ-n/9}$ for an absolute constant $C$. We also obtain a Boolean-circuit compiler with statistical privacy error at most $C\cdot S\cdot 2^{18λ-n/27}$ for $S$ operations and at most $λ$ bits of local leakage per party per operation. The guarantee covers repeated stateful evaluations with adaptively chosen public inputs, with $S$ counting all operations across invocations. Thus, for polynomial-size circuits, a constant leakage fraction is tolerated with share length depending only on the security parameter. We formalize the refreshing bound, the composition and compiler guarantees, and the expected-work bounds in Lean 4. Our results also provide efficient simulation: the leakage can be reproduced from the public inputs and the circuit outputs alone, with expected polynomial overhead.

Leakage-resilient storage encodes a secret as the inner product of two n-bit shares held by separate parties. The shares must be refreshed repeatedly because leakage accumulates. The open question is whether a simple matrix-based refresh is secure under continual local leakage, and whether it supports a circuit compiler with no leak-free components.

In each refresh the left share is multiplied by a uniform invertible matrix M and the right share by M^{-1}. Security is proved by approximating per-round leakage with signed real-valued tables, bounding errors through nuclear-norm and Cauchy–Schwarz arguments, and running a hybrid argument over state labels. The refresh is then used to compile NAND circuits into two-party gadget protocols, including stateful circuits with adaptive public inputs. The main theorems for deterministic strategies are formalized in Lean 4 with Mathlib; the paper states that ChatGPT wrote the formalization.

After T refreshes with λ bits of leakage per party per refresh, the transcripts for two secrets differ in statistical distance by at most C·T·2^{6λ−n/9}. The compiler achieves privacy error at most C·S·2^{18λ−n/27}, with an efficient simulator of expected polynomial overhead. Lean checks the refreshing bound, the compiler composition, the expected-work simulator, and continual stateful privacy.

ApplicationStatistical-distance boundSufficient leakage fraction
Continual refreshing (Thm. 4.1)δ ≤ C·T·2^{6λ−n/9}α < 1/54
Circuit compilation, hidden output shares (Thm. 5.2)δ ≤ C·S·2^{18λ−n/27}α < 1/486
Security bounds and tolerated leakage fractions