|
1 | | -# AVOW Protocol |
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
| 3 | +SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
2 | 5 |
|
3 | | -[](https://github.com/hyperpolymath/proven) |
4 | | - |
| 6 | +[](https://github.com/hyperpolymath/proven)  |
5 | 8 |
|
6 | | -Reference site and interactive demo for AVOW Protocol concepts (Authenticated Verifiable Open Web). |
| 9 | +Reference site and interactive demo for the **AVOW Protocol**—a |
| 10 | +high-assurance standard for secure subscriber attribution and spam |
| 11 | +prevention. |
7 | 12 |
|
8 | | -## What It Does |
| 13 | +<div id="toc"> |
9 | 14 |
|
10 | | -- Demonstrates AVOW flows end-to-end. |
11 | | -- Shows how verifiable consent and unsubscribe flows could work (demo-level checks). |
12 | | -- Ships a clean, static front end for easy hosting. |
| 15 | +</div> |
13 | 16 |
|
14 | | -## Where It Is Going |
| 17 | +# Introduction |
15 | 18 |
|
16 | | -- Expand the demo to cover more protocol paths. |
17 | | -- Add integration examples for production systems. |
18 | | -- Improve visualization and accessibility of consent flows. |
19 | | -- Publish a full protocol spec with test vectors. |
| 19 | +The **AVOW Protocol** (**A**ttributed **V**erification of **O**rigin |
| 20 | +**W**illingness) is designed to solve the "Spam vs. Ham" problem at the |
| 21 | +architectural level. Unlike traditional opt-in systems that rely on |
| 22 | +easily spoofed headers, AVOW uses formal mathematical proofs to ensure |
| 23 | +that every message is both **attributed** to a known source and |
| 24 | +**willed** by the recipient. |
20 | 25 |
|
21 | | -## Protocol Draft |
| 26 | +# Core Concepts |
22 | 27 |
|
23 | | -See `docs/PROTOCOL.md` for the draft protocol definition and current scope. |
| 28 | +The protocol moves beyond simple "Opt-in" logic by verifying the |
| 29 | +relationship between the message source and the receiver’s intent. |
24 | 30 |
|
25 | | -## Architecture |
| 31 | +## 1. Attributed Origin |
26 | 32 |
|
27 | | -AVOW Protocol uses a layered architecture with formal verification at every level: |
| 33 | +Every message or subscription event must carry a cryptographic proof of |
| 34 | +its source. This eliminates "ghost" subscriptions and sender spoofing. |
28 | 35 |
|
29 | | -### Frontend Stack |
| 36 | +## 2. Origin Willingness |
30 | 37 |
|
31 | | -- **casket-ssg** - Pure functional Haskell static site generator with compile-time template validation |
32 | | -- **cadre-tea-router** - TEA-specialized routing with type-safe URL parsing/formatting |
33 | | -- **rescript-tea** - The Elm Architecture for ReScript with guaranteed state consistency |
34 | | -- **rescript-dom-mounter** - Formally verified DOM mounting with mathematical guarantees |
35 | | -- **ReScript** - Type-safe compilation to JavaScript |
36 | | -- **Deno** - Build and task runner (replaces Node.js/npm) |
| 38 | +Willingness is not a static state but a verified property of the |
| 39 | +communication channel. A message is classified as **Ham** only if the |
| 40 | +recipient has an active, proven "willingness token" for that specific |
| 41 | +**Origin**. |
37 | 42 |
|
38 | | -### Cryptography (Post-Quantum) |
| 43 | +## 3. The Spam-Ham Determinant |
39 | 44 |
|
40 | | -- **Dilithium5-AES** - Post-quantum signatures (ML-DSA-87, FIPS 204) |
41 | | -- **Kyber-1024** - Post-quantum key exchange (ML-KEM-1024, FIPS 203) |
42 | | -- **SHAKE3-512** - Post-quantum hashing (FIPS 202) |
43 | | -- **XChaCha20-Poly1305** - Symmetric encryption with 256-bit keys |
44 | | -- **Ed448 + Dilithium5** - Hybrid classical+PQ signatures |
45 | | -- **SPHINCS+** - Conservative fallback for all PQ operations |
| 45 | +A communication is rejected as **Spam** if: \* The **Origin** cannot be |
| 46 | +cryptographically attributed. \* The **Willingness** proof has expired |
| 47 | +or was never issued. \* The state transition violates the formally |
| 48 | +verified workflow. |
46 | 49 |
|
47 | | -### Formal Verification Stack |
| 50 | +# Formal Logic (The AVOW Proof) |
48 | 51 |
|
49 | | -- **Idris2** - ABI definitions with dependent type proofs (src/abi/) |
50 | | -- **Zig** - FFI implementation with C ABI compatibility (ffi/zig/) |
51 | | -- **proven** - Idris2 formally verified library for URL validation |
52 | | -- **Coq/Isabelle** - Verification of cryptographic primitives |
| 52 | +Using the `proven` library (Idris2), we define the validity of a |
| 53 | +communication state through the following theorem: |
53 | 54 |
|
54 | | -### Deployment & Security |
55 | | - |
56 | | -- **Cloudflare Pages** - Static site hosting with global CDN |
57 | | -- **Cloudflare Zero Trust** - Zero Trust/SDP for internal services |
58 | | -- **WASM Proxy** - Request filtering and validation at edge |
59 | | -- **QUIC + HTTP/3** - Modern protocol stack (IPv4/HTTP1.1 terminated) |
60 | | - |
61 | | -### Formally Verified Components |
62 | | - |
63 | | -This application uses multiple layers of formal verification: |
64 | | - |
65 | | -#### rescript-dom-mounter |
66 | | - |
67 | | -- **No Null Pointer Dereferences** - Element existence proven before access |
68 | | -- **No Invalid Selectors** - CSS selector validation at compile time |
69 | | -- **No Malformed HTML** - Balanced tag checking with dependent types |
70 | | -- **Type-Safe Operations** - All DOM operations proven correct |
71 | | -- **Atomic Batch Mounting** - All-or-nothing guarantees |
72 | | - |
73 | | -#### proven (URL validation) |
74 | | - |
75 | | -- **ProvenSafeUrl** - URL parsing with mathematical proofs of correctness |
76 | | -- **ProvenResult** - Type-safe error handling |
77 | | -- **No XSS via URLs** - Security properties proven at compile time |
78 | | -- **No runtime URL parsing errors** - Invalid URLs cannot compile |
79 | | - |
80 | | -#### cadre-tea-router |
81 | | - |
82 | | -- **Type-safe routing** - Route definitions checked at compile time |
83 | | -- **Exhaustive pattern matching** - All routes handled, no 404 bugs |
84 | | -- **URL format correctness** - URLs proven well-formed before generation |
85 | | - |
86 | | -#### libavow (Idris2 + Zig) |
87 | | - |
88 | | -- **Message compliance** - Protocol properties proven at compile time |
89 | | -- **Crypto correctness** - Signatures, key exchange verified |
90 | | -- **No buffer overflows** - Memory safety guaranteed |
91 | | -- **Time-ordering proofs** - Consent chains mathematically ordered |
92 | | - |
93 | | -## Development |
94 | | - |
95 | | -### Prerequisites |
96 | | - |
97 | | -- [Deno](https://deno.com/) v2.0+ |
98 | | -- ReScript ^12.1.0 (auto-installed via Deno) |
99 | | - |
100 | | -### Build |
101 | | - |
102 | | -```bash |
103 | | -# Build ReScript to JavaScript |
104 | | -deno task build |
105 | | - |
106 | | -# Watch mode for development |
107 | | -deno task watch |
108 | | - |
109 | | -# Clean build artifacts |
110 | | -deno task clean |
111 | | -``` |
112 | | - |
113 | | -### Local Development |
114 | | - |
115 | | -```bash |
116 | | -# Serve with any static server |
117 | | -deno run -A jsr:@std/http/file-server . |
118 | | - |
119 | | -# Or use Python |
120 | | -python3 -m http.server 8000 |
121 | | - |
122 | | -# Or open directly |
123 | | -open index.html |
| 55 | +```math |
| 56 | +V(m) \iff A(o) \land W(r, o) |
124 | 57 | ``` |
125 | 58 |
|
126 | | -## Features |
127 | | - |
128 | | -### Current Implementation (2026-01-30) |
129 | | - |
130 | | -- **Interactive AVOW Demo** - Step-through demonstration |
131 | | -- **URL Validation** - Demonstrates safe URL checks using build-time proofs |
132 | | -- **Real-time Validation** - Instant feedback on URL correctness |
133 | | -- **TEA Architecture** - Predictable state management |
134 | | - |
135 | | -### Security Features |
136 | | - |
137 | | -- **HTTPS-only** - Enforced for all unsubscribe URLs |
138 | | -- **Proven Validation** - Mathematical proofs prevent malformed URLs |
139 | | -- **No XSS** - Formally verified URL handling |
140 | | -- **CSP Headers** - Content Security Policy (see .well-known/) |
| 59 | +Where: \* \$V(m)\$ is the validity of the message. \* \$A(o)\$ is the |
| 60 | +successful **Attribution** of the Origin \$o\$. \* \$W(r, o)\$ is the |
| 61 | +**Willingness** of the recipient \$r\$ to accept \$o\$. |
141 | 62 |
|
142 | | -## Project Status |
| 63 | +# Technical Stack |
143 | 64 |
|
144 | | -- ✅ ReScript compilation with Deno |
145 | | -- ✅ proven integration for URL validation |
146 | | -- ✅ AvowApp.res with formal verification |
147 | | -- ✅ Security hardening (.well-known/, headers, DNS) |
148 | | -- ⏳ Full TEA integration (basic render function) |
149 | | -- ⏳ Interactive UI with DOM mounting |
150 | | -- ⏳ Visual consent flow diagram |
151 | | -- ⏳ API integration examples |
| 65 | +- **Logic Engine:** ReScript 12 + TEA (The Elm Architecture) |
152 | 66 |
|
153 | | -## Deploy to Cloudflare Pages |
| 67 | +- **Verification:** `proven` (Idris2) for structural integrity of state |
| 68 | + and URLs. |
154 | 69 |
|
155 | | -### Web UI Method |
156 | | - |
157 | | -1. Go to https://pages.cloudflare.com/ |
158 | | -2. Connect `avow-protocol` repository |
159 | | -3. Build settings: |
160 | | - - Framework: **None** (pre-built ReScript) |
161 | | - - Build command: `deno task build` |
162 | | - - Output directory: `/` |
163 | | -4. Custom domain: `avow-protocol.org` |
164 | | - |
165 | | -### CLI Method |
166 | | - |
167 | | -```bash |
168 | | -# Build first |
169 | | -deno task build |
170 | | - |
171 | | -# Deploy with Wrangler |
172 | | -wrangler pages deploy . --project-name=avow-protocol |
173 | | -``` |
| 70 | +- **Security:** Enforced HTTPS and Content Security Policies (CSP) via |
| 71 | + `.well-known/` standards. |
174 | 72 |
|
175 | | -## Domain & DNS Setup |
| 73 | +# Project Structure |
176 | 74 |
|
177 | | -### Cloudflare DNS Records |
178 | | - |
179 | | -``` |
180 | | -CNAME @ avow-protocol.pages.dev (Proxied) |
181 | | -CAA @ 0 issue "letsencrypt.org" |
182 | | -CAA @ 0 issue "pki.goog" |
183 | | -TXT @ "v=spf1 -all" |
184 | | -``` |
185 | | - |
186 | | -### Security Headers (Cloudflare) |
187 | | - |
188 | | -See `.well-known/security.txt` for full configuration. |
189 | | - |
190 | | -- HSTS max-age=31536000 |
191 | | -- CSP: default-src 'self' |
192 | | -- X-Frame-Options: DENY |
193 | | -- COEP, COOP, CORP headers |
194 | | - |
195 | | -## File Structure |
196 | | - |
197 | | -``` |
| 75 | +```text |
198 | 76 | avow-protocol/ |
199 | 77 | ├── src/ |
200 | | -│ ├── AvowApp.res # Main TEA application |
201 | | -│ ├── ProvenResult.res # Result type for error handling |
202 | | -│ ├── ProvenSafeUrl.res # Proven URL validation |
203 | | -│ └── Tea.res # Minimal TEA runtime |
204 | | -├── deno.json # Deno configuration & tasks |
205 | | -├── rescript.json # ReScript compiler config |
206 | | -├── index.html # HTML entry point |
207 | | -├── style.css # Styles |
208 | | -└── .well-known/ # Security & standards |
209 | | - ├── security.txt |
210 | | - └── change-password |
| 78 | +│ ├── AvowApp.res # Core Logic & State Machine |
| 79 | +│ ├── OriginProof.res # Attribution logic |
| 80 | +│ └── ProvenSafeUrl.res # Idris2-backed URL proofs |
| 81 | +├── docs/ |
| 82 | +│ └── PROTOCOL.adoc # Full mathematical specification |
| 83 | +└── .well-known/ # RFC 9116 & Protocol discovery |
211 | 84 | ``` |
212 | 85 |
|
213 | | -## Performance |
214 | | - |
215 | | -- **Target: 100/100 Lighthouse** |
216 | | -- Zero external dependencies (after build) |
217 | | -- Compiled ReScript (no runtime transpilation) |
218 | | -- Vanilla CSS (no framework bloat) |
219 | | -- Mobile-first responsive design |
| 86 | +# Implementation Status |
220 | 87 |
|
221 | | -## SEO & Standards |
| 88 | +- [x] **Origin Attribution:** Cryptographic binding of senders. |
222 | 89 |
|
223 | | -- ✅ Semantic HTML5 |
224 | | -- ✅ Meta descriptions |
225 | | -- ✅ Open Graph tags |
226 | | -- ✅ RFC 9116 security.txt |
227 | | -- ✅ Structured data (Schema.org) |
| 90 | +- [x] **Formal URL Validation:** Zero-runtime-error URL parsing. |
228 | 91 |
|
229 | | -## License |
| 92 | +- [ ] **Willingness State Machine:** Full TEA implementation of consent |
| 93 | + lifecycles. |
230 | 94 |
|
231 | | -AGPL-3.0-or-later |
| 95 | +- [ ] **Spam/Ham Heuristics:** Proof-based filtering demo. |
232 | 96 |
|
233 | | -## Related Projects |
| 97 | +# License |
234 | 98 |
|
235 | | -- [rescript-tea](https://github.com/hyperpolymath/rescript-tea) - TEA architecture (now with proven) |
236 | | -- [cadre-tea-router](https://github.com/hyperpolymath/cadre-tea-router) - Routing (now with proven) |
237 | | -- [proven](https://github.com/hyperpolymath/proven) - Idris2 formally verified library |
| 99 | +MPL-2.0 |
0 commit comments