Threat Model · EV-010 v1.0.1 · February 2026

REF's Threat Model and Attack Surface

Six adversary archetypes. Fourteen attack scenarios. Three layers of defense. And one honest acknowledgment: the biggest real-world threat isn't a cryptographic break — it's a dishonest merchant.

Prepared by
REF Protocol
Classification
Public
Methodology
RDE (Kiniry et al. 2025)
Artifact
THREAT_MODEL.md · PR #20 merged
The Transparent Threat Statement
The biggest real-world threat isn't a cryptographic break — it's a dishonest merchant fabricating attestations for purchases that never happened. We address this with economics, not cryptography, and we are transparent about that boundary.
01 — Adversary Classes

Six Adversary Archetypes With Modeled Capabilities

Each adversary class has explicit capabilities, constraints, and a primary attack vector. The threat model (THREAT_MODEL.md §3) doesn't just list threats — it bounds what each adversary can and cannot do.

A1 Fraudulent Reviewer High Volume

Motivation: Monetary gain from fake reviews.

Capabilities: Unlimited accounts, scripted behavior, budget for token acquisition.

Primary Vector
Token forgery — break ZK soundness or acquire tokens without valid purchase
A2 Colluding Validators Architecture scenario · requires ≥⌈c/3⌉

Motivation: Undermine consensus for profit or sabotage.

Capabilities (architecture model): Controls ≤ f validators in a committee of size c. EV-008 v1.9 itself uses a fixed Validators set and has no leader, committee, epoch, or VRF state.

Primary Vector
Quorum manipulation — forge QCs, deny service, or approve invalid tokens
A3 Dishonest Merchant Primary Threat

Motivation: Inflate own product ratings with fabricated reviews.

Capabilities: Full admin access to own store. Can sign arbitrary attestations.

Primary Vector
Phantom attestation — sign attestations for purchases that never occurred
A4 Platform Insider Surveillance

Motivation: Deanonymize reviewers, sell behavioral data, or selectively censor reviews.

Capabilities: Full access to platform's token-review database. Can observe token↔review mappings and correlate attestation timestamps with submission timestamps.

Primary Vector
Timing correlation — match attestation issuance time with token submission time to link purchases to reviews
A5 Network Adversary Dolev-Yao

Motivation: Disrupt protocol operation or extract information.

Capabilities: Full network control — intercept, replay, reorder, drop, inject.

Primary Vector
Eclipse attack — isolate validators to prevent quorum formation (liveness)
A6 Cryptographic Adversary Theoretical

Motivation: Break mathematical foundations of the protocol.

Capabilities: Quantum computing, side-channel observation, fault injection.

Primary Vector
PTAU compromise — recover trusted setup toxic waste, forge arbitrary proofs
02 — Threat Entry Points, Ranked

Ordered by Likelihood × Impact

Not all adversaries are equally dangerous. The ranking reflects real-world operational risk, not theoretical worst cases.

1

A3 — Dishonest Merchant: Phantom Attestation

The merchant is trusted to report real purchases (Assumption A-MERCHANT, §2.3). A dishonest merchant can sign attestations for non-existent purchases. The protocol cannot distinguish a real attestation from a fabricated one — both carry valid Ed25519 signatures from the merchant's key.

Vulnerability window: Threat scenario: a Tier 3 merchant may fabricate phantom attestations while attempting to remain within expected volume and evade anomaly detection. The bond system is intended to make modeled attacks economically unattractive under the stated mechanism assumptions; it does not establish a universal real-world profitability result.

PROPOSED / ILLUSTRATIVE CONTROLS: illustrative performance-deposit tiers ($10K/$25K/$50K+) · planned monitoring and platform cross-validation · any forfeiture terms would require a production agreement and attributable evidence
2

A1 — Fake Reviewer: ZK Proof Forgery

Attempting to generate an accepted proof without knowledge of a witness satisfying the configured circuit. A successful attack would require violating the proof-system assumptions or exploiting an implementation or circuit defect; no exact forgery probability is asserted here for the current BN254 instantiation.

MITIGATION: Groth16 verification under stated assumptions · Circuit under-constraint testing (8 recorded negative vectors) · Nullifier uniqueness enforcement
3

A2 (Validator Compromise) / A4 (Platform Deanonymization)

A2 is an architecture-level scenario: corrupting ⌈c/3⌉ validators in a committee, with VRF-based rotation as an intended deployment mechanism. These committee/VRF semantics are not modeled inside EV-008 REFConsensus_v1.9.tla. A4 (Platform Insider) attempts timing correlation to link purchases to reviews. Intended mitigations include batching, delay randomization, and a planned v2 Merkle membership proof to reduce the att_hash correlation vector.

A2 architecture: BFT tolerance (f < c/3) · intended VRF unpredictability · Economic bonds; not an EV-008 modeled-mechanism claim
A4: No PII in public values · Batched submissions · v2 Merkle membership proofs (planned)
The Gap Between Cryptography and Economics

REF's cryptographic layer provides P-AUTH, P-UNIQ, P-INTEG, and P-PRIV — but only under Assumption A-MERCHANT (merchant fidelity). When A-MERCHANT is violated, the system falls back to the economic layer: bonds, monitoring, and contractual forfeiture.

This is a design decision, not a failure. The alternative — requiring the merchant to prove purchases through an untrusted third party — would add infrastructure complexity that kills adoption. REF chooses economic deterrence at the merchant boundary and cryptographic certainty everywhere else.

Documented Privacy Gap — A4 / ATK-4

In v1, att_hash is a public input to the ZK circuit. A colluding merchant + platform pair can match att_hash values between merchant records and token submissions, definitively linking purchases to reviews. This is the documented P-PRIV limitation in THREAT_MODEL.md §ATK-4.

v2 mitigation (planned): att_hash becomes a private input; the public input becomes a Merkle root. The consumer proves att_hash ∈ MerkleTree without revealing which leaf — eliminating the correlation vector entirely.

03 — Security Properties

Six Invariants: Four Cryptographic, Two Economic

Property Type Definition Verification
P-AUTH Crypto Within the token-lifecycle model, provenance-backed review status requires configured eligibility evidence; lawful unverified feedback remains outside that modeled property TokenLifecycle.tla: NoOrphanReview
P-UNIQ Crypto Each purchase entitles at most one review TokenLifecycle.tla: AtMostOneTokenPerPurchase, AtMostOneReviewPerToken
P-INTEG Crypto Finalized tokens and reviews are immutable Cross-layer claim. In TokenLifecycle.tla, the only modeled update to an existing token’s status is RevokeToken, which replaces "valid" with "revoked" and is disabled once a review exists; SubmitReview leaves tokens unchanged and nullifierSet only grows. EV-008 contributes bounded Agreement evidence at MaxView=0; v1.9 has no SafetyInvariant operator. Storage-layer immutability is an implementation obligation and is not established by EV-008 or EV-009.
P-PRIV Crypto No observer learns PII from tokens or proofs ZK soundness: witness hidden by Groth16
P-IC Economic Honest behavior is the dominant strategy DOMINANCE_PROOF.md: α·C₀·N^γ > k · 500 MC runs
P-IR Economic Participation is individually rational Market-justified (FTC penalties $53,088/violation)
Honest Status of P-IR

P-IR (Individual Rationality) is market-justified, not formally proven. We argue that FTC Rule 465 penalties ($53,088 per violation) make platform participation rational, but this is an economic argument, not a mathematical proof. Whether this is a blocking concern or acceptable given the regulatory environment is an open question for external evaluation.

04 — Assume-Guarantee Contracts

What Each Layer Promises and Requires

Following RDE's compositional verification principle, each layer states what it assumes from below and guarantees to above. If an assumption is violated, the degradation mode is explicit — not silent.

🔐
Cryptographic Layer
Attestation + Token + ZK Proof
Guarantees ↑
P-AUTH: Every token bound to purchase
P-UNIQ: One purchase → one review
P-INTEG: The model permits only the "valid" → "revoked" token-status update; SubmitReview leaves tokens unchanged and nullifierSet is append-only. Storage-layer immutability remains an implementation obligation.
P-PRIV: No PII in proofs or tokens
Assumes ↓
A-CRYPTO: Discrete log hardness (BN254)
A-PTAU: ≥1 honest ceremony participant
A-MERCHANT: Purchase attestations are truthful
▼ crypto guarantees feed consensus assumptions
⚡
Consensus Layer
Architecture target: PBFT with rotating committees · EV-008 v1.9 models a fixed validator set
Evidence status ↑
EV-008 CHECKED: Agreement, LockedValueSafety, UniqueHonestProposalPerRound, PrepareVotesReferenceProposals under the bounded MaxView=0 harness
NOT ESTABLISHED BY EV-008: cross-view safety, liveness/fairness, rotating-committee/VRF semantics, or token/review storage immutability
Assumes ↓
ARCHITECTURE A-BFT: f < ⌊c/3⌋ Byzantine per committee (committee semantics not internal to EV-008 v1.9)
ARCHITECTURE A-NET: Partial synchrony / eventual delivery (not modeled by the EV-008 state machine)
Crypto-layer obligations must be imported explicitly at the cross-layer boundary
▼ consensus guarantees feed economic assumptions
💰
Economic Layer
Bonds, monitoring, mechanism design
Guarantees ↑
P-IC: Honesty is dominant strategy
P-IR: Participation is rational
G-DETERRENCE: Fraud is economically irrational
G-DETECTION: Anomalies trigger investigation
Assumes ↓
Dominance: α·C₀·N^γ > k holds
Consensus evidence scoped to its established bounded properties
Crypto soundness (tokens unforgeable)
Cross-Layer Composition — The Key Insight

Economic layer assumes crypto is sound. Crypto layer assumes consensus is safe. If any assumption is violated, the layer above it degrades — but degradation modes are explicit, not silent. This is the assume-guarantee contract documented in THREAT_MODEL.md §6.

05 — Known Refinement-Chain Defects

Engineering Gaps We Found and Documented

Per RDE methodology, a broken refinement chain is a defect — not an adversary attack, but equally dangerous because it prevents the system from delivering its claimed properties. These are tracked with DEF-* identifiers.

DEF-01: Missing att_hash Output from purchase_verification.circom

Severity: P0 engineering gap. Threatens: P-AUTH (purchase binding).

The current purchase verification circuit does not emit att_hash as a circuit output. Without it, the token circuit cannot bind to a verified purchase commitment. Documented in MAPPING.md gap matrix.

DEF-02: Token Spec-to-Circuit Refinement Gap

Threatens: P-AUTH, P-UNIQ, P-PRIV refinement assurance.

EV-011 contains ref_token_v1_1.circom circuit evidence (1,155 constraints; all eight recorded negative vectors were constraint-rejected). The remaining DEF-02 is not a missing-circuit defect: the correspondence between TokenLifecycle.tla state semantics and the Circom constraints is human-maintained, not machine-checked. A change on either side is not automatically proven equivalent. Closing DEF-02 requires a machine-checked refinement/equivalence argument across this spec-to-code boundary.

Why We're Showing You the Defects

These are volunteered, not discovered by audit. They demonstrate that REF's threat model is a living engineering artifact, not a marketing document. Under RDE, documenting what's broken is as important as documenting what works — because you can only fix what you've acknowledged.

"The biggest real-world threat isn't a cryptographic break — it's a dishonest merchant fabricating attestations for purchases that never happened. We address this with economics, not cryptography, and we are transparent about that boundary."
— Core Architectural Principle