Formally Verified Security for PQ-DAS / leanDA

Cryptography
,
1

Formally Verified Security for PQ-DAS

Thanks to Alex Hicks for feedback and discussion.

The post and a detailed security proof outline was written by the human author, the translation to Lean was done with massive help of AI.

Disclaimer. The lean code here proves statements about an abstract scheme, under assumptions about abstract building blocks. In particular, it does not prove security of any production implementation and can never replace proper audit of future implementations.

Motivation and Goal

In a previous post we described and benchmarked a post-quantum data availability sampling (DAS) scheme built from Reed–Solomon codes, hash-based commitments, and the LeanVM proof system. In this post we report on a machine-checked security proof for the cryptographic core of that design: we have formalized the scheme and proven its security in Lean, using mathlib and VCVio, and following the security notions of the Foundations of DAS paper.

The scheme follows the encode-and-prove construction of Section 7 of the Foundations paper, which already comes with a pen-and-paper security proof. However, the scheme we care about makes one non-trivial optimization: instead of proving exact Reed–Solomon membership inside the SNARK, it only proves a cheap probabilistic membership check, whose randomness is derived from the commitment via Fiat–Shamir (outside of the SNARK). The main contribution of the formalization is a full security proof for this optimized variant. This proof is somewhat non-trivial, due to the interplay of random oracles, SNARKs, and rewinding.

TL;DR What we prove

Roughly, we prove the following:

  • Assumptions. We have an erasure code, a secure vector commitment, a random oracle, and a non-interactive argument of knowledge for a relation specified below.

  • Conclusion. We obtain an erasure code commitment scheme that is secure, i.e., position-binding and code-binding, with explicit security reductions.

  • Interpretation. Secure erasure code commitments imply that the resulting DAS scheme is secure, as shown in the Foundations paper (that final compilation step is not formalized).

  • Link to code. Here.

Every reduction in the development is written out as an explicit algorithm, so that a human reader can verify by inspection that it is efficient. The main theorems and where to find them:

Result Lean theorem
Completeness scheme_perfectlyComplete in Target/Scheme.lean
Position-binding scheme_positionBinding in Proof/PositionBinding.lean
Code-binding (modular form) scheme_codeBinding in Proof/CodeBinding.lean
Code-binding (explicit bound) scheme_codeBinding_concrete in Proof/CorollaryCodeBinding.lean

Scheme Abstraction

Why abstraction. We formalize an abstraction of the scheme, e.g., abstracting Merkle trees as vector commitments, following Section 7 of the Foundations paper. We then prove security under assumptions on these abstract building blocks, e.g., position-binding of the vector commitment. The reason is (a) that this covers different variants of the scheme, and (b) that it makes the argument easier to formalize.

Difference to the scheme from the paper. In Section 7 of the Foundations paper, the relation proven by the argument system checks exact membership in the code. Here, we only check an inner product with a random vector of the dual code, derived via Fiat–Shamir. This makes the security proof non-trivial, especially as we cannot rely on extractability of the vector commitment scheme. As we will see, because the vector is derived outside of the SNARK, we can still prove security.

Building Blocks

The scheme uses the following abstract building blocks (each formalized in Assumptions/):

  • An erasure code \mathcal{C} \subseteq \Gamma^n, given by an encoding function \Sigma^k \to \Gamma^n. No further properties of the code are needed for our results: reconstruction-style properties only enter the (non-formalized) step from erasure code commitments to DAS.

  • A vector commitment \mathsf{VC} = (\mathsf{Setup}, \mathsf{Com}, \mathsf{Ver}) satisfying position-binding (Definition 16 in the Foundations paper). We assume \mathsf{Com} and the opening algorithm are deterministic and perfectly complete, which holds for the main instantiation of interest, namely Merkle trees.

  • A code checker (\mathcal{L}, \mathsf{Check}) for \mathcal{C}. This is a new primitive:

    • \mathcal{L} is a finite domain that can be efficiently sampled;

    • \mathsf{Check}(L, c) \to 0/1 takes a domain element L \in \mathcal{L} and an alleged codeword c, and deterministically outputs a bit;

    • Completeness: if c \in \mathcal{C}, then \mathsf{Check}(L, c) = 1 for every L;

    • \delta-Soundness: if c \notin \mathcal{C} is fixed, then \mathsf{Check}(L, c) = 1 with probability at most \delta over a uniformly random L \in \mathcal{L}.

    Intuitively, this models the Reed–Solomon membership check via an inner product from the previous post. Note the order of quantifiers in soundness: the non-codeword is fixed before the randomness is sampled. A cheating committer may correlate its committed vector with the check randomness — this is what we have to rule out in the security proof.

  • A random oracle \mathsf{H} mapping into the domain \mathcal{L} of the code checker.

  • A non-interactive argument of knowledge \mathsf{AS} = (\mathsf{Setup}, \mathsf{Prove}, \mathsf{Ver}) for the relation \mathcal{R} below, satisfying knowledge soundness with a straightline extractor (Definition 18 in the Foundations paper). The relation is:

    • Statement: (\mathsf{ck}, \mathsf{com}_{\mathsf{VC}}, L), i.e., commitment key, commitment, and check randomness;

    • Witness: an alleged codeword c \in \Gamma^n;

    • Constraint: \mathsf{com}_{\mathsf{VC}} = \mathsf{VC}.\mathsf{Com}(\mathsf{ck}, c) and \mathsf{Check}(L, c) = 1.

Note that a full membership check c \in \mathcal{C} is deliberately not part of the relation — this is the whole point of the optimization. One modeling caveat: the argument system is treated as making no random oracle queries itself; when instantiating it with a proof system that internally uses a hash (as LeanVM does), that hash must be domain-separated from \mathsf{H}.

Scheme

With these building blocks, we construct the following erasure code commitment scheme (formalized as scheme in Target/Scheme.lean):

  • \mathsf{Setup}(1^\lambda) \to \mathsf{ck}: run \mathsf{ck}_{\mathsf{VC}} \leftarrow \mathsf{VC}.\mathsf{Setup}(1^\lambda) and \mathsf{par}_{\mathsf{AS}} \leftarrow \mathsf{AS}.\mathsf{Setup}(1^\lambda), return \mathsf{ck} = (\mathsf{ck}_{\mathsf{VC}}, \mathsf{par}_{\mathsf{AS}}).

  • \mathsf{Com}(\mathsf{ck}, m) \to (\mathsf{com}, \mathsf{St}):

    • encode c = \mathcal{C}(m) and commit \mathsf{com}_{\mathsf{VC}} = \mathsf{VC}.\mathsf{Com}(\mathsf{ck}_{\mathsf{VC}}, c);

    • derive L = \mathsf{H}(\mathsf{com}_{\mathsf{VC}});

    • compute \pi = \mathsf{AS}.\mathsf{Prove}(\mathsf{par}_{\mathsf{AS}}, (\mathsf{ck}_{\mathsf{VC}}, \mathsf{com}_{\mathsf{VC}}, L), c);

    • return \mathsf{com} = (\mathsf{com}_{\mathsf{VC}}, \pi).

  • \mathsf{Open} and \mathsf{Ver}: open positions using \mathsf{VC}; verification recomputes L = \mathsf{H}(\mathsf{com}_{\mathsf{VC}}), verifies \pi, and then verifies the opening.

Note that we only hash the commitment to derive L. Hashing more can only make things better in terms of security.

We refer to the Foundations paper for how such a commitment is turned into a DAS scheme; it suffices for the scheme to satisfy code-binding and position-binding, which is what we prove.

Proof Outline

The proof is kind of interesting, so we outline it here. Translating this into lean requires some effort, but not too much. Recall that we want to show position-binding and code-binding (see the Foundations paper for definitions).

Simple: Position-Binding

This directly reduces to position-binding of the vector commitment: the reduction ignores the proof part of the commitment and just forwards the rest (theorem scheme_positionBinding).

Code-Binding: Recap of the proof from the Foundations paper

First recall the security proof if the code check were perfect, i.e., if the relation checked exact code membership:

  • an adversary outputs a commitment (\mathsf{com}_{\mathsf{VC}}, \pi) and openings of some positions so that no codeword is consistent with them;

  • we extract from \pi a preimage c of the commitment \mathsf{com}_{\mathsf{VC}}. As the relation checks exact code membership, c is in the code (otherwise we break knowledge soundness);

  • because c is in the code and no codeword is consistent with the openings, one of the openings must disagree with c — and this breaks position-binding.

For the last step a weak variant of position-binding suffices, in which one of the two openings comes from an honestly computed commitment (namely, the commitment to the extracted c). In the formalization, this weak variant — and also a collision-resistance property of the deterministic \mathsf{Com} used later — are proven from position-binding and completeness (Assumptions/VectorCommitment.lean).

The main technical challenge

In our scheme, code membership is only checked probabilistically, with randomness L derived via Fiat–Shamir from the commitment. Suppose for a moment that the commitment were perfectly extractable: upon seeing \mathsf{com}_{\mathsf{VC}} we could immediately obtain a preimage c that all later openings must be consistent with. Then we could define a bad event for each random oracle query — namely that the queried commitment extracts to a non-codeword c that nevertheless passes the check on the freshly sampled answer L — and bound each such event by \delta, since c is determined before L.

There is an issue with this: think of \mathsf{Com} as a Merkle tree. We evaluate \mathsf{Com} inside the proven relation, but a Merkle tree can only be perfectly extractable if its hash is itself modeled as a random oracle — so we would be evaluating a random oracle inside a proven relation, which requires a relativized succinct argument, shown to be impossible. We must avoid this route. A side note: this is also why the Fiat-Shamir hash is computed outside of the SNARK, otherwise we would be forced to use relativized arguments.

Without extractability, we have no formal guarantee that c is fixed before L is sampled — for all we can prove, the adversary might decide which c to open only after seeing L. So we cannot apply the soundness of the code checker directly.

Intuition for the solution

There is of course hope: if the adversary decides which c to open only after seeing L, then it could just as well have opened a different c' \neq c for a different L' — and two different openings of the same commitment break binding. The problem is that a reduction never sees this hypothetical other c'. The solution is rewinding: run the adversary twice from the point where it produced its commitment, with independent check randomness in the two runs, and make the hypothetical c' actual.

Committed Soundness

We isolate the core of the analysis in an abstract security experiment that we call committed soundness, involving only the vector commitment, the code, the code checker, and the random oracle — the argument system plays no role in it. The adversary gets \mathsf{ck}_{\mathsf{VC}} and access to the random oracle, and outputs a pair (\mathsf{com}_{\mathsf{VC}}, c). With L = \mathsf{H}(\mathsf{com}_{\mathsf{VC}}), it wins if

  1. c \notin \mathcal{C} but \mathsf{Check}(L, c) = 1, and

  2. c commits to \mathsf{com}_{\mathsf{VC}}, i.e., \mathsf{com}_{\mathsf{VC}} = \mathsf{VC}.\mathsf{Com}(\mathsf{ck}_{\mathsf{VC}}, c).

This experiment captures exactly the gap identified above: the adversary may correlate c with the challenge derived from its commitment. (The formalization also contains an equivalent interactive variant without a random oracle, where the game itself sends a uniform L after the adversary commits; the two are related by a standard argument that guesses which oracle query determined the challenge, at a multiplicative loss in the number of queries.)

From Committed Soundness to Code-Binding

Assume for a moment that no efficient adversary can win the committed soundness game. Code-binding then follows by the same pattern as in the Foundations paper (theorem scheme_codeBinding). Let an adversary against code-binding output a commitment (\mathsf{com}_{\mathsf{VC}}, \pi) and openings so that no codeword is consistent with them, and let c be the witness extracted from \pi at the statement (\mathsf{ck}_{\mathsf{VC}}, \mathsf{com}_{\mathsf{VC}}, L). Exactly one of three things happens:

  • Extraction fails (c is not a valid witness): the run breaks knowledge soundness of the argument system (reduction \mathcal{R}_1);

  • Extraction succeeds but c \notin \mathcal{C}: then c passes the check on L = \mathsf{H}(\mathsf{com}_{\mathsf{VC}}) and commits to \mathsf{com}_{\mathsf{VC}} — a win in the committed soundness game (reduction \mathcal{R}_2);

  • Extraction succeeds and c \in \mathcal{C}: since no codeword is consistent with the openings, some opening disagrees with c, breaking (weak) position-binding (reduction \mathcal{R}_3).

A union bound over the three cases gives

\Pr[\text{code-binding broken}] \;\le\; \varepsilon_{\mathsf{ks}} + \varepsilon_{\mathsf{cs}} + \varepsilon_{\mathsf{wpb}}.

Analysis of the Committed Soundness Game

This is the part where we use rewinding (theorem niCommittedSoundness_forking_bound). The idea: if an adversary wins the game with noticeable probability, then — replaying it a second time from the oracle query that determined its challenge, with a fresh answer — it wins both runs with related probability. This is made precise by a forking lemma, which conveniently was already available in the VCVio library. Writing \mathsf{acc} for the winning probability of an adversary making at most Q oracle queries, the two runs yield the same commitment \mathsf{com}_{\mathsf{VC}} with two independent challenges L \neq L' and two answers c, c', and we distinguish:

  • Different answers (c \neq c'): both commit to the same \mathsf{com}_{\mathsf{VC}} under the deterministic \mathsf{Com} — a collision, which breaks position-binding of the vector commitment.

  • Same answer (c = c'): then c was already determined by the first run — in particular before the fresh challenge L' was sampled — and it is a non-codeword passing \mathsf{Check}(L', c) = 1. By \delta-soundness of the code checker, this happens with probability at most \delta.

Overall, the forking analysis yields

\mathsf{acc} \cdot \left( \frac{\mathsf{acc}}{Q+1} - \frac{1}{|\mathcal{L}|} \right) \;\le\; \varepsilon_{\mathsf{coll}} + \delta,

where \varepsilon_{\mathsf{coll}} is the success probability of an explicit collision-finding reduction (which in turn is bounded by position-binding). One pleasant surprise of the formalization effort: analyzing the non-interactive game directly with the library’s forking lemma turned out to be both simpler and quantitatively better than the two-step route through the interactive game sketched above.

The final bound

Combining the pieces and solving the inequality (theorems scheme_codeBinding_concrete and scheme_codeBinding_concrete_posBinding), an adversary breaking code-binding with Q random oracle queries yields

\Pr[\text{code-binding broken}] \;\le\; \varepsilon_{\mathsf{ks}} + \varepsilon_{\mathsf{pb}} + \sqrt{(Q+2)\left(\varepsilon_{\mathsf{pb}}' + \delta + \tfrac{1}{|\mathcal{L}|}\right)},

where \varepsilon_{\mathsf{ks}} is the knowledge soundness error and \varepsilon_{\mathsf{pb}}, \varepsilon_{\mathsf{pb}}' are position-binding errors of explicit reductions. (In the Lean development the bound is stated in an exact squared form, avoiding the square root.)

A remark on the quantitative aspect. The square-root loss and the factor Q are inherent to rewinding-based analyses of Fiat–Shamir-derived randomness, and they matter for parameter selection: the provable security level is governed by \sqrt{Q \cdot \delta} rather than by \delta itself. For instance, a checker with \delta \approx 2^{-136} (as in the Reed–Solomon instantiation of our earlier post) provably provides roughly 36 bits of code-binding security against adversaries making 2^{64} random oracle queries — much more conservative than the heuristic estimate \delta. Maybe this is an artifact of the proof technique, and it remains to be discussed how to set parameters.

What is not covered

The formalization covers the erasure code commitment scheme and its two binding properties, with all reductions explicit. It does not cover: the compilation from erasure code commitments to a full DAS scheme (Section 6 of the Foundations paper), the security of a concrete code checker instantiation (e.g., the barycentric Reed–Solomon check from our earlier post — a natural next step, as its soundness is a self-contained polynomial identity argument), or the internals of the argument system and hash function, which are assumptions of the model.

1 Like