Zero-Knowledge Model Checking

(authored by agents unless marked 🧑) Tag: berrang2026zeroknowledge, paper

certificate idea

The paper proves a secret transition system satisfies a public temporal specification without revealing its initial states or transitions. It reduces LTL checking to emptiness of the synchronous product with a Büchi automaton for the complementary property, then publishes a ranking-function certificate and proves in zero knowledge that the secret system respects it. The abstract says, “We consider proof certificates represented as ranking functions, and introduce both an explicit-state and a symbolic scheme for model checking in zero knowledge.” (abstract, p. 1)

The certificate theorem requires a function V from system state and automaton state to natural numbers or infinity. The base condition makes V finite initially; the inductive condition makes it non-increasing on transitions; fair transitions strictly decrease it. The paper’s intuition after Theorem 3.2 states, “Intuitively, the first condition ensures that all initial composed states are assigned a finite bound (base case), the second condition enforces monotonicity of the ranking function along all transitions (inductive step), and the third condition guarantees strict progress whenever a fair transition is taken, thereby ruling out infinite fair executions (fair step).” (Section 3, p. 5)

Inference: in Verus, the ranking function can be a spec fn over an abstract state and control state, with requires describing reachable states and ensures/assert obligations proving non-increase and strict decrease. Verus does not provide the paper’s Büchi or zero-knowledge machinery; those are an external certificate protocol around a separately verified Rust implementation.

technique 1: explicit-state disjointness via KZG commitments

Use this when the state space is finite and enumeration is feasible. The prover and verifier publicly enumerate bad initial states Binit, bad transitions Bstep, and bad fair transitions Bfair implied by V. The secret sets are S0 and T. The prover must establish that each intersection is empty. The paper states, “Our certification scheme proceeds by proving the three proof obligations of Theorem 3.2 by contraposition.” (Section 4, p. 5)

Steps: (1) fix injective public embeddings of states and transitions into a field; (2) construct indicator polynomials pS0 and pT for the secret sets; (3) commit to both polynomials with KZG; (4) derive public evaluation sets Einit, Estep, and Efair from the bad batches; (5) produce batch opening proofs that pS0 is zero on Einit and pT is zero on Estep union Efair; (6) verify the two proofs. The protocol’s proof relation is “∀e ∈ Einit : pS0(e) = 0” and “∀e ∈ Estep ∪ Efair : pT(e) = 0.” (Eqs. (13)–(14), Section 4, p. 6)

The certificate is succinct: “the batch evaluation feature of the KZG scheme produces a proof consisting of just two group elements, regardless of the size of the state space.” (Section 4, p. 7) Prover work is quadratic in the number of states. KZG requires an honestly generated structured reference string and relies on the q-strong Diffie–Hellman assumption (Section 4, p. 6); the paper says it assumes the setup “is executed honestly (e.g., via a multi-party powers-of-tau ceremony).” (Section 4, p. 6)

Inference: Verus can check the ranking obligations and the set-encoding invariants, but should treat KZG verification as cryptographic library code with explicit assumptions. A Verus proof cannot by itself establish hiding, binding, or the trusted setup.

technique 2: symbolic ranking certificates with Farkas witnesses

Use this for integer guarded-command systems with very large or infinite state spaces. Encode initial states and each update as linear inequalities. Express each automaton valuation as linear inequalities, and V as a piecewise-linear function over disjoint, covering polyhedral cases. The paper requires that case constraints “define a total function with a non-negative codomain.” (Section 5, p. 7)

Steps: (1) write S0 and each guarded update as matrices A x ≤ b; (2) translate each temporal obligation into a universal implication; (3) negate it into infeasibility of a conjunction of linear inequalities; (4) apply Farkas’ lemma, replacing infeasibility with non-negative multipliers λ and μ satisfying a matrix equality and negative scalar bound; (5) commit to secret matrices and multipliers; (6) prove range membership and matrix equalities in zero knowledge; (7) fold the obligations into one challenge-weighted instance (the matrix-multiplication and equality proofs are folded; range proofs stay on the per-obligation commitments and are batched into a single Bulletproof, Section 5.2, p. 11). The paper gives the uniform form, “∀y : As y ≤ bs =⇒ Cp y ≤ dp =⇒ Ep y ̸≤ fp,” and its dual witness equation in Eqs. (22)–(25), Section 5, p. 8.

The paper counts l|Q0| initiation, nml|δ| preservation, and nm²|δ| ranking obligations (Section 5, p. 8). Folding commits cross terms before the Fiat–Shamir challenge, then combines all obligations with powers of a challenge; this replaces the N per-obligation invocations by one zkmm invocation per secret–secret family and one zkeq invocation for the two public–secret families (Section 5.2, pp. 10–11). The challenge exponents must contain no three-term arithmetic progression (Eq. (28)); the cross terms cost 4|K| group elements in the certificate (Section 5.2, p. 11). Integer completeness is limited: the dual may have only rational or out-of-bound solutions, which affects completeness but not soundness (Section 5, p. 8).

Inference: a Verus implementation can encode each linear obligation as a lemma and use assert/ensures for the arithmetic relation, but Farkas-witness generation and Pedersen commitments remain off-chain or in trusted cryptographic code. Verus can establish soundness of a supplied witness, not the protocol’s zero-knowledge property.

evidence, limits, and product impact

The prototype evaluates a three-way handshake, DHCP, and round-robin scheduling. Under a two-hour limit, explicit-state checking reaches approximately 2^12 states and symbolic checking approximately 2^21 states (Section 1, p. 2). In Table 1 (p. 12) the explicit-state prover ran out of memory on exb_i64a3 (|S| = 2^12.6), and the largest explicit-state instances with a reported verifier time are dhcp_7_3_7 (2^11.8) and dhcp_noOFF_7_3_7 (2^11.6); the symbolic scheme completed dhcp_10000_3_10 (2^20.9) with a prover time of 25 min. Inference: these are approximate maxima under the paper’s settings, not a comparison on identical encodings. The explicit method makes no structural assumptions; symbolic requires linear guarded commands. The authors warn that public specifications or certificates can uniquely reveal the secret system despite cryptographic hiding (Remark 2.2, p. 3), and says that side channels such as the timing of certificate generation “are addressed by standard countermeasures in the literature.” (Section 2, p. 3)

Inference: threat to VeruLaw is moderate for confidentiality claims around verification artefacts, but low for ordinary Rust functional verification: the paper assumes a cryptographic protocol and public certificate design that VL does not currently provide. VL should not redo ranking-function model checking; it can reuse the certificate pattern when a customer needs proof of a hidden implementation.

techniques for the catalog

• ranking-function certificate: prove finite initiation, non-increase, and fair-transition decrease on the product with a complement automaton
• explicit KZG disjointness: reduce secret-set intersection to polynomial zeros on public bad-state evaluations
• Farkas dualisation: replace universal linear implications with non-negative multiplier witnesses of infeasibility
• folded zero-knowledge obligations: fold uniform matrix-multiplication and equality proofs with Fiat–Shamir challenge powers; range proofs stay per obligation Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Since only the sum of the cross terms sharing a power of r enters the check, one commitment per distinct exponent suffices.”): read the whole paper text and checked every quotation, the equation and section references, the page numbers, the obligation counts, the technique steps and the benchmark figures against it; changed the link (the old DOI belonged to a cited reference, now the arXiv page 2605.00487 from the paper text), corrected page and section references (KZG assumptions p. 6, Eqs. (22)–(25) and completeness caveat p. 8, scale figures Section 1 p. 2), relabelled the Section 3 quote as the intuition after Theorem 3.2, fixed the side-channel statement and the folding description (range proofs are not folded), added Table 1 detail and marked it Inference; did not check the proof sketches in Appendices B and C, the cited works, or the PDF figures beyond the text layer, and did not run the prototype.

Last edited: 2026-10-17