proofs/tamarin/ZKVerification.spthy

/*
 * Zero-Knowledge Proof Verification Protocol (Z-Chain)
 * Formal model in Tamarin Prover
 *
 * Protocol source:
 *   ~/work/lux/consensus/protocol/quasar/ (ZK-based certificate compression)
 *   General ZK proof system (Groth16 / Plonk style)
 *
 * Protocol:
 *   Setup:
 *     CRS (Common Reference String) generated by trusted setup
 *     CRS published publicly; contains proving key and verification key
 *
 *   Proving:
 *     Prover has statement x and witness w such that R(x, w) = true
 *     Prover computes proof pi = Prove(pk, x, w)
 *     Prover sends (x, pi) to verifier
 *
 *   Verification:
 *     Verifier checks Verify(vk, x, pi) = true
 *     Verifier accepts x without learning w
 *
 * Tamarin abstraction choices:
 *   - Relation R(x, w) modeled as: relation(x, w) = true iff valid pair
 *   - Proof generation: zk_prove(pk, x, w) -> pi (only works if R(x, w) holds)
 *   - Verification: zk_verify(vk, x, pi) -> true (only if pi was honestly generated)
 *   - Simulation: zk_simulate(sim_trapdoor, x) -> pi_sim (for ZK property)
 *   - Extraction: zk_extract(ext_trapdoor, pi) -> w (for soundness proof)
 *   - CRS: setup(trapdoor) -> (pk, vk)
 *
 * Security goals:
 *   1. Soundness: no valid proof for a false statement
 *   2. Zero-knowledge: verifier learns nothing beyond statement truth
 *   3. Completeness: honest prover always convinces honest verifier
 *   4. Non-malleability: cannot derive new proofs from existing ones
 *
 * Copyright (C) 2019-2026, Lux Industries Inc. All rights reserved.
 */

theory ZKVerification
begin

builtins: hashing

/*
 * ==================================================================
 * Function symbols
 * ==================================================================
 */

functions:
  /* Trusted setup */
  zk_pk/1,              /* zk_pk(trapdoor) -> proving_key */
  zk_vk/1,              /* zk_vk(trapdoor) -> verification_key */

  /* Relation (statement, witness) */
  relation/2,           /* relation(x, w) -> true if R(x, w) holds */

  /* Proof system */
  zk_prove/3,           /* zk_prove(pk, x, w) -> proof pi */
  zk_verify/3,          /* zk_verify(vk, x, pi) -> true/fail */

  /* Simulation (for ZK property: simulator can make proofs without witness) */
  zk_simulate/2,        /* zk_simulate(trapdoor, x) -> simulated proof */

  /* Extraction (for soundness: extractor can pull witness from proof) */
  zk_extract/2,         /* zk_extract(trapdoor, pi) -> witness */

  /* Statement commitment (binds proof to specific statement) */
  commit_statement/2    /* commit_statement(x, nonce) -> commitment */

/*
 * ==================================================================
 * Equations
 * ==================================================================
 */

equations:
  /* Correct verification: honestly generated proof verifies */
  zk_verify(zk_vk(td), x, zk_prove(zk_pk(td), x, w)) = true,

  /* Simulated proofs also verify (ZK property: indistinguishable) */
  zk_verify(zk_vk(td), x, zk_simulate(td, x)) = true,

  /* Extraction from honest proof recovers witness */
  zk_extract(td, zk_prove(zk_pk(td), x, w)) = w

/*
 * ==================================================================
 * Restrictions
 * ==================================================================
 */

restriction Equality:
  "All x y #i. Eq(x, y) @ i ==> x = y"

restriction ValidRelation:
  "All x w #i. ProvedRelation(x, w) @ i
   ==> (Ex #j. RelationHolds(x, w) @ j & j < i)"

/*
 * ==================================================================
 * Rules
 * ==================================================================
 */

/*
 * Trusted Setup: generate CRS from trapdoor.
 * Trapdoor must remain secret; if leaked, soundness is broken.
 */
rule Trusted_Setup:
  let pk = zk_pk(~trapdoor)
      vk = zk_vk(~trapdoor)
  in
  [ Fr(~trapdoor) ]
  --[ SetupComplete(~trapdoor, pk, vk),
      SecretTrapdoor(~trapdoor) ]->
  [ !ProvingKey(pk),
    !VerificationKey(vk),
    !Trapdoor(~trapdoor),
    Out(pk),
    Out(vk) ]

/*
 * Establish Relation: register a valid (statement, witness) pair.
 * This models the existence of a satisfying assignment.
 */
rule Establish_Relation:
  [ Fr(~x), Fr(~w) ]
  --[ RelationHolds(~x, ~w) ]->
  [ !ValidPair(~x, ~w),
    Out(~x) ]
  /* Note: witness ~w is NOT output -- only prover knows it */

/*
 * Prover: generates proof for valid statement.
 * Only succeeds if the prover knows a valid witness.
 */
rule Generate_Proof:
  let pi = zk_prove(pk, x, w)
  in
  [ !ProvingKey(pk),
    !ValidPair(x, w) ]
  --[ ProvedRelation(x, w),
      ProofGenerated(x, pi) ]->
  [ Out(<x, pi>) ]

/*
 * Verifier: checks proof against verification key.
 * Accepts the statement without learning the witness.
 */
rule Verify_Proof:
  [ In(<x, pi>),
    !VerificationKey(vk) ]
  --[ Eq(zk_verify(vk, x, pi), true),
      ProofVerified(x, pi) ]->
  [ ]

/*
 * Corrupt Setup: adversary obtains trapdoor.
 * This should only break the system if explicitly modeled.
 */
rule Corrupt_Setup:
  [ !Trapdoor(td) ]
  --[ TrapdoorLeaked(td) ]->
  [ Out(td) ]

/*
 * ==================================================================
 * Lemmas
 * ==================================================================
 */

/*
 * Completeness: honest prover with valid witness always convinces verifier.
 */
lemma completeness:
  exists-trace
  "Ex x pi #p #v.
    ProofGenerated(x, pi) @ p &
    ProofVerified(x, pi) @ v &
    p < v"

/*
 * THEOREM 1: Soundness
 *
 * If a proof is verified for statement x, then either:
 *   (a) there exists a valid witness (the relation holds), or
 *   (b) the trusted setup trapdoor was leaked (system broken)
 *
 * No valid proof exists for a false statement under honest setup.
 */
lemma soundness:
  "All x pi #v.
    ProofVerified(x, pi) @ v
    ==>
    ( (Ex w #r. RelationHolds(x, w) @ r)
    | (Ex td #l. TrapdoorLeaked(td) @ l & l < v) )"

/*
 * THEOREM 2: Zero-Knowledge (Witness Secrecy)
 *
 * The verifier learns nothing about the witness beyond the fact that
 * the relation holds. Modeled as: the witness w remains secret even
 * after the proof is verified, unless the adversary already knew it.
 *
 * The only way the adversary learns w is if it was directly revealed
 * (not through the proof).
 */
lemma zero_knowledge_witness_secrecy:
  "All x w #r.
    RelationHolds(x, w) @ r &
    not(Ex #k. K(w) @ k)
    ==>
    /* w stays secret even after proofs about x are verified */
    not(Ex pi #v #k2.
      ProofVerified(x, pi) @ v &
      K(w) @ k2)"

/*
 * THEOREM 3: Soundness Without Trapdoor
 *
 * Strictly: if the trapdoor is never leaked, then every verified
 * proof corresponds to a true statement.
 */
lemma soundness_no_trapdoor:
  "All x pi #v.
    ProofVerified(x, pi) @ v &
    not(Ex td #l. TrapdoorLeaked(td) @ l)
    ==>
    (Ex w #r. RelationHolds(x, w) @ r)"

/*
 * THEOREM 4: Simulation Indistinguishability
 *
 * A simulated proof (using trapdoor) is as valid as an honest proof.
 * This is the formal basis of zero-knowledge: the verifier's view
 * can be simulated without the witness.
 *
 * Existence trace: simulator produces a valid proof.
 */
lemma simulation_indistinguishability:
  exists-trace
  "Ex td x pi #s #v #l.
    TrapdoorLeaked(td) @ l &
    ProofVerified(x, pi) @ v &
    SetupComplete(td, zk_pk(td), zk_vk(td)) @ s &
    s < l & l < v"

end