avow-protocol

AVOW Protocol: Attributed Verification of Origin Willingness

Idris Inside Protocol Draft

Reference site and interactive demo for the AVOW Protocol—a high-assurance standard for secure subscriber attribution and spam prevention. Table of Contents

Introduction
Core Concepts
    1. Attributed Origin
    2. Origin Willingness
    3. The Spam-Ham Determinant
Formal Logic (The AVOW Proof)
Technical Stack
Project Structure
Implementation Status
License

Introduction

The AVOW Protocol (Attributed Verification of Origin Willingness) is designed to solve the "Spam vs. Ham" problem at the architectural level. Unlike traditional opt-in systems that rely on easily spoofed headers, AVOW uses formal mathematical proofs to ensure that every message is both attributed to a known source and willed by the recipient. Core Concepts

The protocol moves beyond simple "Opt-in" logic by verifying the relationship between the message source and the receiver’s intent. 1. Attributed Origin

Every message or subscription event must carry a cryptographic proof of its source. This eliminates "ghost" subscriptions and sender spoofing. 2. Origin Willingness

Willingness is not a static state but a verified property of the communication channel. A message is classified as Ham only if the recipient has an active, proven "willingness token" for that specific Origin. 3. The Spam-Ham Determinant

A communication is rejected as Spam if: * The Origin cannot be cryptographically attributed. * The Willingness proof has expired or was never issued. * The state transition violates the formally verified workflow. Formal Logic (The AVOW Proof)

Using the proven library (Idris2), we define the validity of a communication state through the following theorem: \[V(m) \iff A(o) \land W(r, o)\]

Where: * V ( m ) is the validity of the message. * A ( o ) is the successful Attribution of the Origin o . * W ( r , o ) is the Willingness of the recipient r to accept o . Technical Stack

Logic Engine: ReScript 12 + TEA (The Elm Architecture)

Verification: proven (Idris2) for structural integrity of state and URLs.

Security: Enforced HTTPS and Content Security Policies (CSP) via .well-known/ standards.

Project Structure

avow-protocol/ ├── src/ │ ├── AvowApp.res # Core Logic & State Machine │ ├── OriginProof.res # Attribution logic │ └── ProvenSafeUrl.res # Idris2-backed URL proofs ├── docs/ │ └── PROTOCOL.adoc # Full mathematical specification └── .well-known/ # RFC 9116 & Protocol discovery

Implementation Status

✓ Origin Attribution: Cryptographic binding of senders.

✓ Formal URL Validation: Zero-runtime-error URL parsing.

❏ Willingness State Machine: Full TEA implementation of consent lifecycles.

❏ Spam/Ham Heuristics: Proof-based filtering demo.

License

PMPL-1.0-or-later

I’m going to pressure-test this against what already exists and where the idea breaks against reality. I’m assuming you mean email/newsletter/subscription flows first, because “spam vs ham” gets slippery fast outside that; if you meant SMS/telephony instead, say so and I’ll retarget it.

This is already clarifying itself: origin-attestation is real and standardized territory; recipient-willingness is the part that’s novel, but also the part most likely to bite you. I’m pulling the current mail standards and bulk-sender rules so I can tell you whether AVOW is a real gap or just a fancy wrapper around DKIM/DMARC + unsubscribe.

You’re not a fool. This is a real instinct hitting a real gap. But in its current form, AVOW is trying to prove something the mail ecosystem usually can’t prove cleanly.

Email already has a pretty mature stack for origin-side claims: SPF authorizes sending hosts, DKIM signs mail at the domain level, DMARC aligns authenticated identities with the visible From domain, and ARC exists because forwarding, mailing lists, and other intermediaries routinely break simpler authentication models. Mailing-list UX also already has standardized List-Subscribe and List-Unsubscribe headers, with RFC 8058 defining one-click unsubscribe. Large receivers like Gmail now explicitly require bulk senders to use SPF, DKIM, DMARC alignment, TLS, and one-click unsubscribe for marketing/subscribed mail.

So AVOW is not solving a fake problem. The real gap is this: origin authentication is standardized; recipient willingness is mostly handled as policy, reputation, UX, and local receiver judgment, not as a portable cryptographic fact. Even Google’s current guidance leans on opt-in, confirmation, unsubscribes, and spam complaint rates, and explicitly notes that the line between promotional and transactional mail depends partly on recipient context. The email architecture docs also make clear that user-level behavior and mailing-list behavior are messy and partly subjective, not something you can reduce to one timeless global truth.

That’s the core problem in your theorem: V(m)  ⟺  A(o)∧W(r,o) V(m)⟺A(o)∧W(r,o)

A(o) is plausible. W(r,o) is the dangerous bit. A protocol can prove a token exists. It cannot really prove, in the human sense, that a recipient is still “willing” right now, in this context, for this exact message class, through this route, after forwarding, delegation, mailing-list remailing, account compromise, or changing preferences.

The spots where AVOW currently overreaches are these:

It treats ham/spam as if it were fully derivable from origin + consent, when receivers also care about reputation, abuse, complaints, compromise, and message class.

It assumes a neat sender→recipient path, but SMTP has relays, gateways, mediators, and mailing lists that can re-post or modify messages while preserving some original authorship cues. ARC exists precisely because intermediaries break simpler authentication stories.

It puts a lot of emphasis on HTTPS/CSP/.well-known, but transport security and discovery territory is already occupied by things like MTA-STS and current sender requirements. That’s useful plumbing, just not your differentiator.

It wants a binary proof where the real world probably needs graded attestation. Telephony’s STIR/PASSporT/SHAKEN stack is a good precedent here: it uses cryptographic origin identity plus levels of attestation, not a magical absolute truth bit.

Here’s the salvage, and I think it’s actually pretty good:

AVOW should stop pretending to be a universal “spam killer protocol” and become a consent-attested messaging framework for subscribed/bulk/managed communication.

That means: V(m,t)  ⟺  Attest(o,s,m) ∧ ConsentCap(r,o,purpose,channel,t) ∧ Fresh(cap,t) ∧ NotRevoked(cap,t) ∧ ReplaySafe(m,cap) ∧ WorkflowOK V(m,t)⟺Attest(o,s,m) ∧ ConsentCap(r,o,purpose,channel,t) ∧ Fresh(cap,t) ∧ NotRevoked(cap,t) ∧ ReplaySafe(m,cap) ∧ WorkflowOK

That is much stronger. It says:

the origin is attested,

the sender is authorized to act for that origin,

the recipient previously granted a scoped capability,

the capability is fresh and not revoked,

the message can’t replay an old proof,

and the state machine is valid.

That is no longer “is this ham in the philosophical sense?” It is “does this message satisfy a formally checkable acceptance policy?” That’s actually implementable.

My honest verdict:

As a universal internet protocol: probably too ambitious, and a bit category-confused. As a domain-scoped or provider-scoped protocol for consent-attested bulk mail / subscriptions / list traffic: genuinely interesting.

The practical version of AVOW would look like this:

Origin attestation token
Signed by the sender domain, or by a delegated ESP with explicit delegation.

Recipient willingness token
Really this should be a consent capability, not “willingness” in the philosophical sense. It should be scoped to:

recipient pseudonym or mailbox handle

origin

list or purpose

allowed message class

expiry

revocation reference

nonce / anti-replay binding

Receiver policy engine
Receiver verifies both tokens and then still applies local policy.

Graceful coexistence with mail today
AVOW should ride alongside SPF/DKIM/DMARC/ARC, not replace them.

The other big recommendation: keep Idris inside the verifier, not inside the wire protocol identity. Formal methods are excellent for proving your parser, state machine, and token-validation rules are sound. They do not prove that remote parties are honest, or that human consent semantics are complete.

So the sharp version is:

Good idea: consent as a cryptographically scoped capability.

Weak idea: “spam vs ham solved architecturally.”

Best framing: “AVOW is a formally specified, consent-attested extension for subscribed messaging, not a universal theorem of wantedness.”

If I were steering the repo, I’d rewrite the pitch to:

AVOW is a consent-attested messaging framework that combines authenticated origin, delegated sender authority, and recipient-scoped acceptance capabilities for high-assurance subscription and bulk-mail workflows.

That pitch is strong. The current one is a little too “I have abolished spam by theorem,” which is catnip for reviewers in the wrong way.

Next thing I’d write is the threat model before any more code: attacker goals, trust anchors, token issuer, delegation model, replay model, revocation model, mailing-list/forwarder behavior, and downgrade story.

could you write me a replacement README.adoc

Absolutely — here’s a replacement README.adoc that pitches AVOW in a sharper, more credible way, without sounding like it’s trying to mathematically abolish spam from the universe.

AVOW Protocol

AVOW — Attributed Verification of Origin & Willingness — is a high-assurance protocol draft for consent-attested messaging.

Rather than attempting to "solve spam" in the abstract, AVOW defines a verifiable acceptance model for messages that should only be delivered when two conditions hold:

1. the sender’s origin can be cryptographically attributed; and

2. the recipient has a valid, scoped, non-revoked willingness token for that origin and message purpose.

AVOW is aimed at subscription, notification, and managed messaging workflows where consent, attribution, and policy enforcement need to be explicit, inspectable, and machine-verifiable.

1. Status

Important

AVOW is currently a protocol exploration and reference implementation draft. It is not a replacement for SMTP, SPF, DKIM, DMARC, ARC, or existing unsubscribe standards. It is best understood as a complementary consent-attestation layer for high-assurance messaging environments.

Current state:

• ✅ Origin attribution model drafted

• ✅ Formal validation experiments with Idris2 / proven

• ✅ Initial ReScript architecture for stateful protocol demos

• ❏ Willingness capability model in progress

• ❏ Revocation / expiry lifecycle design in progress

• ❏ End-to-end protocol demo not yet complete

2. Why AVOW?

Existing messaging systems are reasonably good at proving aspects of sender identity, but much weaker at proving whether a recipient has actually granted ongoing, scoped permission for a class of messages.

That creates a familiar mess:

• spoofed or weakly-attributed origins

• stale or unverifiable consent records

• ambiguous subscription state

• poor replay / revocation semantics

• "opt-in" claims that are hard to independently verify

• overloading of local spam filtering with consent questions it cannot cleanly prove

AVOW explores a stricter model:

\$V(m, t) iff A(o) and C(r, o, p, t) and F(c, t) and R(m, c) and S\$

Where:

• V(m, t) = message m is valid for acceptance at time t

• A(o) = origin o is cryptographically attributed

• C(r, o, p, t) = recipient r has a valid consent capability for origin o and purpose p

• F(c, t) = the capability is fresh / unexpired at time t

• R(m, c) = the message and capability are replay-safe

• S = the state transition satisfies the verified workflow

This is intentionally narrower than "all ham/spam classification". AVOW is about provable acceptance conditions, not universal philosophical certainty about wantedness.

3. Core Concepts

3.1. 1. Attributed Origin

Every accepted communication must be bound to a cryptographically attributable origin.

This means:

• the sender identity is not merely asserted in a mutable header

• the sending authority can be tied to a recognized origin

• delegated senders can be modeled explicitly rather than hand-waved

AVOW treats unattributed or ambiguously attributed origin as a first-class failure.

3.2. 2. Willingness as a Capability

AVOW does not treat willingness as a vague boolean preference. Instead, it models willingness as a scoped capability with explicit properties such as:

• recipient

• origin

• purpose or message class

• channel

• issuance time

• expiry time

• revocation reference

• anti-replay binding

A message is not accepted merely because a sender once claimed "the user opted in". It must correspond to a currently valid willingness capability.

3.3. 3. Verified State Transitions

Consent is not static. It changes over time through a lifecycle such as:

• requested

• challenged

• granted

• renewed

• narrowed

• revoked

• expired

AVOW models these transitions explicitly so that invalid state jumps can be rejected.

3.4. 4. Spam/Ham as Policy Outcome

AVOW deliberately avoids claiming that all spam detection can be reduced to one theorem.

Instead:

• AVOW can prove whether a message satisfies a strict consent-attested acceptance policy

• receivers may still apply local reputation, abuse, content, and operational policy

That distinction matters. AVOW is a high-assurance protocol component, not a magic replacement for receiver judgment.

4. Protocol Model

At a high level, AVOW introduces two linked proofs:

1. Origin Proof — this message originates from an attributable sender or authorized delegate

2. Willingness Proof — this recipient has granted a valid, scoped capability for this class of communication

A receiver evaluates both before deciding whether a message qualifies for AVOW acceptance.

Sender/Delegate
   |
   | 1. emits attributed message + origin proof
   | 2. binds message to willingness capability reference
   v
Receiver
   |
   |-- verify origin attribution
   |-- verify willingness capability
   |-- check expiry / revocation / replay safety
   |-- validate workflow state transition
   v
Accept / Quarantine / Reject

5. Design Principles

5.1. Explicit over implicit

No hidden "trust me, the user signed up somewhere" semantics.

5.2. Scoped consent over blanket consent

Permission should be narrow, inspectable, and purpose-bound.

5.3. Formal workflow integrity

State transitions should be specified precisely enough to verify.

5.4. Coexistence over replacement

AVOW should layer alongside existing mail and messaging infrastructure, not pretend the last 20 years never happened.

5.5. High assurance where it matters

The goal is not maximal complexity everywhere. The goal is to make strong guarantees possible in systems that actually need them.

6. Non-Goals

AVOW is not trying to be:

• a universal replacement for SMTP

• a replacement for SPF, DKIM, DMARC, or ARC

• a complete spam-filtering engine

• a proof of human intent in the philosophical sense

• a guarantee that a message is good, useful, or non-abusive in all contexts

AVOW is specifically about cryptographically and structurally verifiable acceptance criteria.

7. Technical Stack

The current reference site / demo stack uses:

• ReScript 12 + TEA for the protocol demo and state machine UI

• Idris2 with proven for high-assurance validation experiments

• AsciiDoc for protocol documentation

• .well-known/ conventions for discovery and policy surfacing

• HTTPS + CSP for secure reference-site delivery

The formal methods work is intended to strengthen the protocol model and verifier logic. It is not a claim that formal proofs alone eliminate operational abuse.

8. Repository Structure

avow-protocol/
├── src/
│   ├── AvowApp.res         # Core application and protocol state machine
│   ├── OriginProof.res     # Origin attribution logic
│   ├── Willingness.res     # Consent capability lifecycle (planned/in progress)
│   └── ProvenSafeUrl.res   # Idris2-backed safe URL integration
├── docs/
│   ├── PROTOCOL.adoc       # Full protocol draft
│   ├── THREAT-MODEL.adoc   # Adversaries, trust boundaries, and failure modes
│   └── STATE-MACHINE.adoc  # Consent lifecycle and transition rules
└── .well-known/
    ├── security.txt
    └── avow                # Discovery / policy experiments

9. Implementation Priorities

Near-term priorities:

1. define the willingness capability schema

2. specify revocation and renewal semantics

3. model replay resistance

4. document delegation rules for third-party senders

5. write the threat model before over-building the demo

6. produce a minimal end-to-end verifier

Suggested milestone sequence:

• M1 — Formalize origin attribution structure

• M2 — Define willingness capability format

• M3 — Specify state transitions and invalid transitions

• M4 — Implement verifier prototype

• M5 — Build demo showing accept / reject / revoke paths

• M6 — Evaluate interoperability with real-world mail flows

10. Threat Model

AVOW is only meaningful if it states what it is defending against.

Key threat categories include:

• forged or weakly attributed sender identity

• stale or fabricated consent claims

• replay of previously valid capabilities

• revoked-but-still-used willingness proofs

• confused deputy problems with delegated senders

• state-machine bypasses

• downgrade to non-AVOW delivery semantics

A dedicated threat model document is strongly recommended and should be treated as a core protocol artifact, not an afterthought.

11. Example Acceptance Rule

An AVOW-aware receiver might evaluate a message using logic like:

accept(message) if
  verifyOrigin(message.originProof) &&
  verifyCapability(message.willingnessProof) &&
  capabilityMatches(message.origin, message.recipient, message.purpose) &&
  !isExpired(message.willingnessProof) &&
  !isRevoked(message.willingnessProof) &&
  !isReplay(message)
else reject_or_quarantine(message)

This is intentionally stricter than common marketing-email workflows. That is the point.

12. Project Philosophy

AVOW assumes that secure messaging should not depend entirely on:

• sender self-description

• vague claims of prior opt-in

• reputation systems alone

• after-the-fact unsubscribe flows

Instead, it explores whether origin and recipient willingness can be made explicit enough to verify.

That makes AVOW especially relevant to systems that value:

• strong consent guarantees

• auditable subscription workflows

• formally specified transitions

• abuse-resistant notification channels

• research into high-assurance messaging infrastructure

13. Development

deno task build
deno task watch

As the protocol matures, this repository is expected to contain:

• a reference site

• an interactive protocol demo

• a verifier prototype

• formal notes and proofs

• threat-model documentation

• example issuer / receiver flows

14. Contributing

Contributions are welcome, especially in these areas:

• protocol design review

• threat modeling

• formal specification

• ReScript implementation

• Idris2 proof support

• interoperability critique

• naming and scope refinement

The most useful feedback is the brutal kind: tell us where the model breaks, where the assumptions leak, and where the protocol is pretending to know more than it really can.

15. License

This project is licensed under:

PMPL-1.0-or-later

See the license file for full terms.

I can also do a tighter second pass that sounds more like one of your repo READMEs — more manifesto-ish, more formal-methods-heavy, or more “Rhodium standard / protocol-draft” in tone.