Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Security Definitions

The proof map traces verifier soundness — the deployed Halo 2 verifier under Zcash/Snark/. This page is its companion for the other half of the development: the protocol security properties under Zcash/Security/ — binding-signature balance, key binding, and the ledger-model security games — and how each one connects, by reduction, to a primitive hardness assumption and to the verifier-soundness proof.

Every argument here has the same shape, the development-wide breaks as computed data convention:

A security property, if violated, exhibits a concrete break of an underlying primitive — a discrete-log relation, a hash collision, a commitment-opening collision — computed as data. Hardness is assumed only at the computational layer, against the exhibited break.

So each definition sits on a three-layer stack:

  • Layer A — vocabulary. The break events, as structures carrying their data (RandomOracle.Collision, NontrivialRelation, NoteCommitBreak). Deterministic; no probability.
  • Layer B — reduction. A computable def that turns a property violation into a Layer-A break (NontrivialRelation.ofImbalance, Merkle.collisionOfWrongLeaf, noteCommitBreakOfNe). Deterministic; no hardness assumption.
  • Layer C — probability. The bound that producing the break is hard: the birthday bound q(q-1)/|F|, or the discrete-log advantage. The only layer that consumes an assumption.

One connected picture

%%{init: {"flowchart": {"nodeSpacing": 20, "rankSpacing": 50, "padding": 6, "diagramPadding": 4, "subGraphTitleMargin": {"top": 4, "bottom": 18}}, "themeCSS": ".cluster-label { font-weight: 700; font-size: 1.1em; font-family: raleway, sans-serif; }"}}%%
flowchart TD
  subgraph GAMES["Ledger security games — the capstones"]
    BAL["Balance<br/>balanceSubsetOrBreak<br/>balanceValueOrBreak"]
    SPEND["Spendability<br/>faerieGoldCore<br/>validLedger_append"]
    SPENDAUTH["Spend authority<br/>spendAuthorityOrBreak"]
  end

  BAL --> BS["Binding-signature<br/>balance"]
  BAL --> NCB["Note-commitment<br/>binding"]
  BAL --> MERK["Merkle-path<br/>binding"]
  BAL --> KB["Key binding<br/>ZIP 2005 (ROM)"]
  SPEND --> NCB
  SPEND --> MERK
  SPEND --> KB
  SPEND --> NFB["Nullifier binding"]
  SPENDAUTH --> KB

  subgraph ASSUMPTIONS["Hardness assumptions"]
    DL[("Discrete log")]
  end

  subgraph MODELS["Heuristic adversary models"]
    ROM[("Random oracle")]
  end

  BS --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/BindingSignature/Balance.lean'>non-balancing<br/>bundle computes</a>"| NDLR["NontrivialRelation<br/>(V,R) discrete-log<br/>relation"]
  BS --> STMT["Witness or replay<br/>evidence<br/>ActionSatisfied<br/>§4.17.4"]
  NCB --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Statement.lean'>wrong note<br/>opening computes</a>"| NCBK["NoteCommitBreak"]
  NCB --> STMT
  MERK --> STMT
  MERK --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Merkle.lean'>wrong Merkle<br/>path computes</a>"| MC["DefinedCollision<br/>(one height, encoding<br/>domain, success-only)"]
  KB --> STMT
  KB --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/KeyBinding/Basic.lean'>conflicting ivk<br/>witnesses compute</a>"| CUS["CollisionUpToSign<br/>shifted oracle,<br/>distinct queries"]
  NFB --> STMT
  NFB --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Spendability.lean'>distinct derive-inputs +<br/>equal nullifier<br/>computes</a>"| NFC["NullifierCollision"]
  SPENDAUTH --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/SpendAuthority.lean'>verified signature over<br/>unsigned sighash computes</a>"| SAF["SpendAuthForgery<br/>(randomization<br/>of ±ak)"]

  STMT -. "<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Snark/Soundness/Composition/Bridge.lean'>justified by<br/>the extractor;<br/>hencodes gap</a>" .-> KS["Knowledge soundness:<br/>accepting proof yields<br/>witness or break data"]
  NCBK --> SDLR["Sinsemilla<br/>discrete-log<br/>relation"]

  NDLR -->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Snark/Soundness/AGM/BindingSignature.lean'>independent<br/>hash-to-curve bases</a>"| DL
  SDLR -->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Snark/Soundness/AGM/BindingSignature.lean'>independent<br/>hash-to-curve bases</a>"| DL
  KS --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Snark/Soundness/AGM/Capstone.lean'>AGM heuristic +<br/>independent<br/>hash-to-curve bases</a>"| DL
  KS -->|"<a target='_blank' href='https://github.com/zcash/ironwood/tree/main/Zcash/Snark/Soundness/Forking'>Fiat–Shamir<br/>heuristic</a>"| ROM
  MC --> SDLR
  CUS --->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Common/Birthday.lean'>birthday counting<br/>q(q-1)/r,<br/>no assumption</a>"| ROM
  NFC -->|"<a target='_blank' href='https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Nullifier.lean'>distinct-note openings<br/>compute</a>"| SDLR
  SAF --> RDSA["RedDSA unforgeability,<br/>±-randomized keys"]
  RDSA -->|"re-rand reduction<br/><a target='_blank' href='https://eprint.iacr.org/2015/395'>[FKMSSS2016]</a> +<br/>forking extraction"| DL
  RDSA -->|"challenge hash<br/>as random oracle"| ROM

  click BAL "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Balance.lean" _blank
  click SPEND "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Spendability.lean" _blank
  click SPENDAUTH "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/SpendAuthority.lean" _blank
  click BS "https://github.com/zcash/ironwood/blob/main/Zcash/Security/BindingSignature/Balance.lean" _blank
  click NCB "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Statement.lean" _blank
  click MERK "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Merkle.lean" _blank
  click KB "https://github.com/zcash/ironwood/blob/main/Zcash/Security/KeyBinding/Basic.lean" _blank
  click NFB "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Spendability.lean" _blank
  click STMT "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Statement.lean" _blank
  click NCBK "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Statement.lean" _blank
  click MC "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Merkle.lean" _blank
  click CUS "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Common/RandomOracle.lean" _blank
  click NFC "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/Spendability.lean" _blank
  click SAF "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Ledger/SpendAuthority.lean" _blank
  click NDLR "https://github.com/zcash/ironwood/blob/main/Zcash/Common/DiscreteLogRelation.lean" _blank
  click SDLR "https://github.com/zcash/ironwood/blob/main/Zcash/Common/DiscreteLogRelation.lean" _blank
  click KS "https://github.com/zcash/ironwood/blob/main/Zcash/Snark/Soundness/KnowledgeSoundness.lean" _blank
  click DL "https://github.com/zcash/ironwood/blob/main/Zcash/Common/DiscreteLogRelation.lean" _blank
  click ROM "https://github.com/zcash/ironwood/blob/main/Zcash/Security/Common/RandomOracle.lean" _blank
  click RDSA "https://github.com/zcash/ironwood/issues/22" _blank

  classDef proven fill:#1a7f37,stroke:#116329,color:#ffffff
  classDef checked fill:#0969da,stroke:#0550ae,color:#ffffff
  classDef partial fill:#9a6700,stroke:#7d4e00,color:#ffffff
  classDef hyp fill:#cf222e,stroke:#a40e26,color:#ffffff
  classDef assumed fill:#57606a,stroke:#424a53,color:#ffffff
  class BAL,SPEND,SPENDAUTH,KS partial
  class NCB,BS,KB,MERK,NFB,STMT,NDLR,CUS,NCBK,MC,NFC,SAF checked
  class SDLR,RDSA hyp
  class DL,ROM assumed

■ fully proven — nothing here yet
■ stated and machine-checked in Lean, over abstract primitives
■ partly machine-checked; remainder tracked (the games' probabilistic capstones; knowledge soundness's hencodes bridge)
■ named hypothesis; formalization deferred
■ assumption or heuristic model; terminal by design

This picture is a deliberate approximation, and is likely to change as the formalization proceeds. The RedDSA node is a named hypothesis rather than a terminal assumption: its discharge edge names the reduction for security of signatures with re-randomizable keys [FKMSSS2016, section 3], adapted to the ±-randomized variant, together with forking extraction of the Schnorr witness.

Every solid arrow reads "rests on"; where an edge carries a label, the label names the computed break object flowing along it, or the adversary model or side condition under which the reduction holds (the AGM restriction, base independence from hash-to-curve, the birthday count). The games are the top-level capstones. The ledger model requires the adversary to supply, along with any accepting proof, a witness or replay evidence for the Action statement (ActionSatisfied) — in the replay case the ledger oracle can produce the previously supplied witness. Each component argument consumes the statement's satisfaction on that witness. Knowledge soundness is what justifies the modelling: whenever the ledger layer needs a witness, the extractor computes one —or computes break data— from the accepting proof. The dashed edge marks that justification, which crosses the hencodes gap — "gate satisfaction implies the intended high-level statement". The latter is the subject of the circuit soundness proof.

The definitions

Binding-signature balance — value preservation
balanceSecurity.BindingSignature.Balance
No transaction creates or destroys value (spec §4.13 Sapling / §4.14 Orchard). Value commitments are cv v rcv = v • V + rcv • R; a bundle's binding verification key collects to bvk = A • V + B • R with A the net value imbalance. The property is not "no discrete-log relation between V and R exists" — one always does in a prime-order group — but the reduction below.
NontrivialRelationBindingSignature.NontrivialRelation · .ofImbalance
The break, as computed data: a nontrivial F-linear relation between the value base V and randomness base R. ofImbalance (and the bundle forms ofBundleModImbalance, ofOrchardImbalance, ofSaplingImbalance) computes one from a non-balancing verifying bundle, with no cryptographic hypothesis — equivalently the discrete log dlog_R V (imbalance_yields_discrete_log).
integer no-overflow liftintBalance_eq_zero_of_lt · orchard_natAbs_lt · sapling_natAbs_lt
Lifts field balance (A = 0 in ZMod r) to integer balance: with per-action 64-bit value ranges and a bounded action count, |A| < r, so the residue being zero forces the integer to be zero. Discharged per pool from the value-type subranges.
reduces to DLSnark.Soundness.AGM.BindingSignature
Turns the computed Orchard/Sapling relations into plain discrete-log solutions: if you can unbalance, you can solve DL. DLR and DL are tightly equivalent (Jaeger–Tessaro, 2020/1213, Lemma 3), so this assumes no more than DL hardness, given the independence of the hash-to-curve bases.
Key binding — ZIP 2005 theorem (ROM)
key bindingSecurity.KeyBinding.KB
A verifying Recovery-Statement witness pins its key components — ak (up to y-sign), nk, and the qk/sk branch with its key — to ivk, unless a break is exhibited (ZIP 2005 key-binding theorem). Factors as KB = KBOpening ∧ KBDerivation: the Commit^ivk opening and the derivation constraints.
commit_scalar_pmKeyBinding.commit_scalar_pm · OpeningBreak
Algebraic core: two openings of the same Commitivk value force their Pedersen scalars equal or negated. An OpeningBreak (two valid openings differing in the opening data) is the break structure the games layer produces.
reduces to an RO collisionCollisionUpToSign.ofBreak · Birthday.birthday_closed_form
The reduction computes a ±-collision of the rivk-derivation random oracle at distinct derivation queries from a break (Layer B). Producing that collision within q queries is bounded by the birthday bound ε_kb ≤ q(q-1)/r (Layer C).
Ledger-model games — the abstract Action statement
Action statement satisfiedSecurity.Ledger.ActionSatisfied
The games-relevant conjuncts of an Orchard-shaped Action statement (spec §4.17.4) over abstract primitives: commitment integrity, Merkle-path validity, nullifier integrity, the key-binding condition, address integrity, value-commitment integrity. This is the interface the games consume, and the target the verifier-soundness proof is meant to deliver.
pinning lemmasivk_pinned · nk_eq_or_break · nf_old_eq_or_break
The deterministic steps of the Balance argument: an address (g_d, pk_d) determines ivk (needs only g_d ≠ 0 and torsion-freeness), hence nk is determined up to an exhibited key-binding break, and spends of the same note tuple reveal the same nullifier up to a break.
NoteCommitBreakLedger.NoteCommitBreak · noteCommitBreakOfNe
A note-commitment opening collision, as data. noteCommitBreakOfNe computes one when an extract-equal commitment fails to pin the note tuple (rcm, note). Prequantumly, note-commitment binding reduces to a Sinsemilla / discrete-log-relation break.
Merkle position bindingLedger.Merkle.collisionOfWrongLeaf
Fixed-depth Merkle trees are position-binding up to a hash collision: a validating authentication path for a leaf that is not the committed one, against a defined tree, computes a DefinedCollision of one height’s compression — escaped (⊥) evaluations never count as collisions. The vector-commitment property the Balance and Spendability arguments require of the note-commitment tree. Prequantumly, the Sinsemilla compression’s collision resistance reduces to a discrete-log-relation break (SDLR) — the same terminal as note-commitment binding — so BLAKE2b collision resistance does not enter the pre-quantum Balance argument.
Shared foundation · Zcash/Security/Common
collision vocabularySecurity.RandomOracle.Collision · CollisionUpToSign
Layer-A break events for the classical ROM: a Collision is two distinct queries with equal outputs; a CollisionUpToSign (a =± b) is the shape produced by arguments passing through the Extract coordinate extractor, whose fibres are {P, −P}. Key binding bottoms out here, as does the nullifier (Faerie-Gold) argument for the Recovery Statement; the deployed nullifier argument bottoms out in the Sinsemilla discrete-log relation instead.
birthday boundSecurity.Birthday.birthday_closed_form
The Layer-C probability: the shifted ±-collision event over q uniform oracle outputs has probability at most q(q-1)/|F|, by union-bounding the per-pair fraction 2/|F|. Counted in the random-oracle model with no hardness assumption; proven as a probability statement over the uniform oracle table (#73).

New to the shorthand? See the Glossary.  ·  For the verifier-soundness half, the Proof Map.