mirror of
https://github.com/block/buzz.git
synced 2026-08-18 06:50:31 +02:00
Multi-tenant relay: spec + mechanized formal proof (S1–S8) (#1285)
Signed-off-by: Tyler Longwell <tlongwell@block.xyz> Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@sprout-oss.stage.blox.sqprod.co> Co-authored-by: Tyler Longwell <tlongwell@block.xyz> Co-authored-by: Mari <95cae996907d7cab9f5dbf43c0f53edeac6ab0b032a6feae4abfd784e467b3f5@sprout-oss.stage.blox.sqprod.co> Co-authored-by: npub1mprnacetjua2xx3p5eddmhxyk6wv929ymm5py8kd2xfxurxahspqqlgyta <d8473ee32b973aa31a21a65adddcc4b69cc2a8a4dee8121ecd51926e0cddbc02@sprout-oss.stage.blox.sqprod.co> Co-authored-by: npub1jmc9dt2lyvzu3h0kxlwxt5zg4fxp9476awyxw6gwxn72g6cw7exqs64whm <96f056ad5f2305c8ddf637dc65d048aa4c12d7daeb8867690e34fca46b0ef64c@sprout-oss.stage.blox.sqprod.co>
This commit is contained in:
Tyler
co-authored by
npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d
Tyler Longwell
Mari
npub1mprnacetjua2xx3p5eddmhxyk6wv929ymm5py8kd2xfxurxahspqqlgyta
npub1jmc9dt2lyvzu3h0kxlwxt5zg4fxp9476awyxw6gwxn72g6cw7exqs64whm
npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d
Tyler Longwell
Mari
npub1mprnacetjua2xx3p5eddmhxyk6wv929ymm5py8kd2xfxurxahspqqlgyta
npub1jmc9dt2lyvzu3h0kxlwxt5zg4fxp9476awyxw6gwxn72g6cw7exqs64whm
parent
34b2d3e8b4
commit
2ecdcce7bd
@@ -0,0 +1,74 @@
|
||||
# Multi-tenant Conformance Checklist
|
||||
|
||||
This document is the source-vs-model checklist for adding first-class communities
|
||||
without changing the observed behavior of a single-community Buzz deployment.
|
||||
|
||||
The compatibility rule is: **today's Buzz is one implicit community selected by
|
||||
its relay URL**. Multi-tenant Buzz makes that selector explicit at the backend
|
||||
boundary while preserving the Nostr wire format, existing REST paths, channel
|
||||
UUIDs, event shapes, media URLs, git Smart HTTP behavior, workflow behavior, and
|
||||
CLI/Desktop/MCP expectations when `N = 1`.
|
||||
|
||||
## Row zero: request community binding
|
||||
|
||||
Every external request starts with exactly one community:
|
||||
|
||||
> `req.community = resolve_host(connection.host)`, bound at connection
|
||||
> establishment, before any WebSocket `EVENT`/`REQ`, REST handler, media handler,
|
||||
> git transport handler, webhook handler, workflow side effect, search query, or
|
||||
> pub/sub fan-out path observes tenant data.
|
||||
|
||||
Conformance obligations:
|
||||
|
||||
- The URL host is the authoritative community selector. This preserves today's
|
||||
"the relay URL is the thing I connected to" semantic while lifting it one
|
||||
level up from relay process to community.
|
||||
- Unknown or unmapped hosts fail closed with a generic rejection; they never fall
|
||||
through to a default tenant.
|
||||
- NIP-98/API-token/community stamps may narrow or authenticate authority, but
|
||||
they never override the host-derived community. A token whose community stamp
|
||||
disagrees with `req.community` is rejected.
|
||||
- A client-supplied `h` tag is adversarial input. If present, it must resolve to
|
||||
a channel inside `req.community`; if absent, the event is channel-less but still
|
||||
community-scoped as `community_id = req.community`.
|
||||
- The single-community deployment is the degenerate case: one configured host
|
||||
resolves to the one default community, so existing clients observe the same
|
||||
behavior.
|
||||
|
||||
## Conformance table
|
||||
|
||||
| Surface | Today's observable behavior | Tenant source | Community-global vs operator-global | Required DB/index/RLS scope | Auth/fan-out/search effects | Single-community compatibility check | Open decision/test |
|
||||
|---|---|---|---|---|---|---|---|
|
||||
| Row zero: host binding | A user connects to one relay URL and all state they can observe belongs to that relay. | `resolve_host(connection.host)` before handler entry. | Community-global selector; operator only manages the host map. | `communities(host, id, signing_key, …)`; every scoped table references immutable `community_id`. | All auth, event, REST, media, git, search, pub/sub, and workflow paths consume `TenantContext`; host/token mismatch rejects generically. | One host maps to the default community; no client-visible protocol field changes. | Add model/prose gate that `ctx.community` is derived from host, not supplied by the client. |
|
||||
| NIP-11 relay info and relay `self` | `GET /`/`/info` returns one relay info document; `RelayInfo::build` advertises static NIPs and a stable relay signing pubkey when configured. | Host-derived community for community-specific facts; no DB lookup from unauthenticated global state unless explicitly through `TenantContext`. | NIP-11 is community-global. Operator-global software/version may be shared; relay `self` for group/system/audit signing is per-community. | `communities.signing_key` or equivalent per-community signing material; no platform-global `self` for tenant-observable system events. | Unauthenticated reads must not become enumeration oracles for other communities. NIP-43 advertisement reflects membership enforcement for that community only. | One community returns the same JSON except for values already configured today. | Signature/static-input lint remains: `RelayInfo::build` must not grow unscoped DB/search/audit inputs. |
|
||||
| API tokens and NIP-98 replay | API/NIP-98 clients authenticate REST/media/git; API tokens may carry scopes and channel IDs; NIP-98 replay uses an in-process seen-set today. | Host-derived community plus token's stamped community; stamps must agree. | Community-global token namespace; operator-global only for deployment health/secrets. | `api_tokens` gains `community_id`; token hash uniqueness and lookup are `(community_id, token_hash)` or the token cryptographically embeds community and lookup verifies both. Channel claims must reference channels in the same community. | Replay seen-set key is `(community_id, event_id)` in shared HA storage or equivalent sticky routing; NIP-98 `u` URL host must match `req.community`. | Existing single-community tokens continue to authorize the same scopes/channels after backfill to default community. | HA gate: Redis/shared seen-set with atomic insert-if-absent and TTL ≥ replay window, or documented single-replica/sticky alternative. |
|
||||
| Relay membership, pubkey allowlist, archived identities | `relay_members`, `pubkey_allowlist`, and `archived_identities` are relay-global gates over pubkeys. | Host-derived community for tenant access; operator context only for platform administration. | Community-global membership/allowlist/archive by default. Operator-global only for explicit platform ops tables that are never tenant-observable. | Add `community_id` to these tables; primary/unique keys become `(community_id, pubkey)` and indexes include `community_id`. | Membership errors remain generic. NIP-OA owner checks test owner membership in the same community. Identity archive requests cannot hide/archive a key in another community. | One default community preserves today's closed/open relay behavior and admin CLI semantics after commands target the default community. | Decide any future operator-global super-admin surface separately; do not reuse tenant membership tables for it. |
|
||||
| Users, profiles, NIP-05, and user search | Kind:0 updates sync a `users` row; NIP-05 handles are unique; `/api/users/search` searches display name/NIP-05/pubkey. | Channel-less events use `req.community`; NIP-05 domain is the connected community host. | Community-global. Same pubkey can have one profile per community; users repost kind:0 in each community they join. | `users` gains `community_id`; keys/uniques are `(community_id, pubkey)`, `(community_id, lower(nip05_handle))`, and `(community_id, okta_user_id)` where applicable. Profile event replacement is scoped by `(community_id, pubkey)`. | Search and batch profile reads include `community_id`; NIP-05 lookup only resolves handles for the requested host/community. No cross-community profile inheritance. | Existing users backfill into the default community; profile APIs and CLI output stay unchanged. | Add tests for same pubkey with different profile/NIP-05 in two communities and for NIP-05 same local part on two hosts. |
|
||||
| Channel-less global events and DMs | Events with `channel_id = NULL` include profiles, DMs, lists, status, long-form, engrams, membership notifications, workflow commands, and repo announcements; global subscriptions use p/kind gates. | `req.community` when no `h` tag is present. | Community-global. "Global" means visible across channels inside one community, never across communities. DMs are per-community. | `events`, `event_mentions`, replaceable/NIP-33 indexes, reactions, thread metadata, feed tables, and direct ID lookup helpers include `community_id`. NIP-33 uniqueness is `(community_id, kind, pubkey, d_tag)`. | `REQ`, `/query`, `/count`, feed, direct `GET /api/events/{id}`, deletes, reactions, and thread lookups filter by community before event id/pubkey/kind matching. | Single-community global subscriptions and DMs still behave as today. | Regression tests for same event id/d-tag/pubkey in two communities and for DM `#p` not cross-delivering. |
|
||||
| Channels and channel membership | `channel_id` (`h` tag) is the only locality boundary; channels, membership, canvas, topic, DMs, NIP-29 discovery are channel-scoped. | `resolve(h)` must equal `req.community`; channel creation writes `community_id = req.community`. | Community-global channel namespace; channel-local for channel content. | `channels`, `channel_members`, canvas/topic/DM participant hashes, NIP-29 group ids, and channel indexes include `community_id`. `channels.community_id` is immutable. | Mixed-community or unknown `h` tags reject generically. Open-channel discovery lists only channels in the community. | Existing channel UUIDs and `h` tags remain valid after default-community backfill. | Migration lint forbids channel re-tenanting except through an explicitly modeled admission path. |
|
||||
| Workflows, runs, approvals, webhooks, schedules | Workflows are channel-scoped or project/channel-global; triggers fire on matching stored events; schedule/webhook/manual triggers create runs; approval tokens are hashed. | Workflow definition's community from `req.community` at create/update; webhook/schedule/manual routes resolve workflow id inside host-derived community. | Community-global workflow namespace; runs/approvals inherit workflow community. | `workflows`, `workflow_runs`, `workflow_approvals` include `community_id`; workflow id/token hash lookups are scoped; trigger event ids are scoped. | Trigger evaluation only sees events in the same community. Webhook URLs include host-derived community; approval token grants cannot act on another community's same hash/id. | Existing workflow APIs and YAML remain unchanged in default community. | Add tests for identical workflow UUID/approval token hash in different communities and schedule execution isolation. |
|
||||
| Search / Typesense | One collection (`events`) indexes `id`, `content`, `kind`, `pubkey`, optional `channel_id`, `created_at`, `tags_flat`; channel-less docs use `__global__`; relay refetches canonical events from Postgres by hit id. | Search query carries `req.community`; indexed documents carry `community_id`. | Community-global search results; operator-global collection infrastructure may be shared. | Typesense schema adds faceted `community_id`; document id is collision-safe (`community_id:event_id`) or deletes/upserts always include a community filter. Postgres refetch uses `(community_id, event_id)`. | Every `filter_by` includes `community_id:=…` plus channel scope. `__global__` means channel-less within the community, not platform global. | One community can use the same collection and produce the same search results. | Reindex gate required; tests for same event id/content in A and B, deletion in A not deleting B. |
|
||||
| Redis pub/sub, presence, typing, and cache invalidation | Event fan-out uses `buzz:channel:{uuid}`; presence uses `buzz:presence:{pubkey}`; typing uses `buzz:typing:{channel_id}`; cache invalidation uses `buzz:cache-invalidate`. | Pub/sub calls receive `TenantContext` and derive keys from `community_id` plus channel/pubkey. | Pub/sub and presence are community-global; Redis deployment is operator-global shared infrastructure. | Redis keys include community: `buzz:{community}:channel:{uuid}`, `buzz:{community}:presence:{pubkey}`, `buzz:{community}:typing:{channel_id}`, and community-aware cache invalidation payloads/channels. | Cross-node fan-out must not deliver events to subscriptions in another community. Same pubkey can be online/away differently in two communities. Cache drops only affect same-community membership/visibility caches unless explicitly all-community operator maintenance. | Single-community can preserve existing key names only if deployment is isolated; shared multi-tenant Redis must use the prefixed form. | Add tests for same pubkey presence in two communities and same channel UUID collision in two communities. |
|
||||
| Media / Blossom / S3 | Authenticated uploads return content-addressed descriptors; public `GET/HEAD /media/{sha256.ext}` serves blobs; upload audit has `channel_id = None`. | Upload request host provides `req.community`; Blossom/NIP-98 auth URL host must agree. | Blob CAS bytes may be operator-global shared storage; metadata, authorization, quotas, audit, and visibility are community-global. | Media metadata/audit rows include `community_id`; if object keys stay SHA-addressed, any per-community policy lives outside the raw blob key. | Upload/read authorization uses community context. Shared hash bytes are allowed only as dedup/storage optimization; metadata/errors must not reveal another community's private upload. | Existing media URLs keep working for default community. | Decide whether unauthenticated blob `GET` remains intentionally public; if not, reads need host-scoped auth/visibility checks. |
|
||||
| Git hosting / NIP-34 / object storage | Smart HTTP at `/git/{owner}/{repo}` hydrates from S3 object pointers; NIP-34 repo announcements use `d=repo-id`; pointer key is `repos/{owner}/{repo}/pointer`; git push emits kind:30618. | Git HTTP host gives `req.community`; NIP-98 URL and repo announcement community must agree. | Community-global repo namespace and NIP-34 state; pack/manifests CAS objects may be operator-global if pointers are scoped. | Pointer/name keys include community, e.g. `repos/{community}/{owner}/{repo}/pointer`; NIP-34 replaceable coords include `community_id`; any repo-name registry is `(community_id, owner, repo)` or `(community_id, repo)` per product rule. | Clone/push/read policy resolves repo and branch protections only inside the host community. Git hook policy callback carries community and rejects mismatches. | Existing clone URLs and repo ids work under the default community; object-store migration can move pointers under default prefix without changing git clients. | Add tests for same owner/repo in two communities and push in A not advancing B pointer. |
|
||||
| Mesh, agents, ACP/MCP, and CLI | Agents/CLI connect to a relay URL and use WS/REST; mesh/pairing/presence/status events are regular signed relay events. | The relay URL/host configured in the agent/CLI session selects community. | Agent membership, persona/profile, presence, jobs, memory events, and mesh status are community-global unless a future operator mesh plane is explicitly separate. | Any persisted agent profile/job/mesh status rows/events use `community_id`; Redis/presence/search keys follow the same community scoping. | A portable key may join multiple communities, but memberships, DMs, profiles, jobs, and presence do not bleed across them. | Existing `BUZZ_RELAY_URL` continues to select the one default community. | Add CLI/ACP smoke tests against two hosts using same key with different memberships/profile. |
|
||||
| Audit log and observability | One hash-chain audit log records event/channel/auth/media actions; errors are sanitized before reaching clients. | Every tenant-observable audit entry is labeled with `req.community` or inherited community from the object being acted on. | Community-global audit chains; operator metrics/log aggregation may be platform-global only if tenant labels are bounded and access-controlled. | `audit_log` key/sequence/head includes `community_id`; error/audit projection tables include `community_id`; uniqueness is `(community_id, seq)` and `(community_id, hash)` as appropriate. | Audit reads verify only one community chain. Error strings must not include cross-community IDs, constraint names, or existence facts. | Single-community audit verification still traverses one chain. | Eva owns model edits here; infra lane must ensure media/git/token/search rows emit community-labeled audit entries. |
|
||||
|
||||
## Migration gates
|
||||
|
||||
Before multi-tenant mode is admitted, the implementation must have automated gates
|
||||
for these classes of mistakes:
|
||||
|
||||
1. Every tenant-scoped table has `community_id`, RLS policy, and no unique/FK
|
||||
constraint that can be observed across tenants unless explicitly admitted as
|
||||
operator-global.
|
||||
2. Every direct lookup by event id, token hash, workflow id, approval token,
|
||||
repo pointer/name, media hash metadata, pubkey profile, or channel id also
|
||||
carries community context or first resolves the object under community.
|
||||
3. Every cache/search/pubsub/object-store key that can affect tenant-visible
|
||||
observations includes community context, except for deliberately shared CAS
|
||||
byte storage whose authorization metadata is community-scoped.
|
||||
4. Every externally reachable handler obtains `TenantContext` from host binding
|
||||
before reading request body data that can cause tenant effects.
|
||||
5. N=1 conformance tests prove existing clients do not need new tags, paths,
|
||||
event fields, CLI flags, or protocol messages to keep current behavior.
|
||||
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1,6 @@
|
||||
# TLC model-checker scratch output (fingerprint/state dirs, per-run).
|
||||
# Generated by `tlc` runs of MultiTenantRelay.tla; not part of the artifact.
|
||||
states/
|
||||
*.st
|
||||
*.fp
|
||||
tla2tools.jar
|
||||
@@ -0,0 +1,748 @@
|
||||
theory MultiTenantAuth
|
||||
begin
|
||||
|
||||
builtins: signing, hashing
|
||||
|
||||
// ============================================================================
|
||||
// Multi-tenant relay auth/key/audit model (draft skeleton)
|
||||
// ============================================================================
|
||||
//
|
||||
// This model covers the symbolic security surface for the multi-tenant relay:
|
||||
// NIP-98 minting, stamped bearer-token use, per-community signing keys, and
|
||||
// independent per-community audit chains. It intentionally follows the house
|
||||
// style of crates/buzz-core/src/pairing/NIP-AB.spthy: explicit adversary/leak
|
||||
// rules, action facts for theorem statements, and reachability / anti-vacuity
|
||||
// lemmas near the bottom.
|
||||
//
|
||||
// Final theorem wording is expected to be tightened by the prose contract in
|
||||
// docs/multi-tenant-relay.md. Until then these lemmas are the intended shape,
|
||||
// not the final public statement.
|
||||
|
||||
// Tamarin has no primitive != in lemma conclusions; model inequality through an
|
||||
// action fact guarded by a global restriction. Rules emit Neq(x,y) only at the
|
||||
// comparison point relevant to the counterexample.
|
||||
restriction Inequality:
|
||||
"All x #i. Neq(x, x) @ i ==> F"
|
||||
|
||||
restriction Equality:
|
||||
"All x y #i. Eq(x, y) @ i ==> x = y"
|
||||
|
||||
// ============================================================================
|
||||
// Setup: communities, channels, clients
|
||||
// ============================================================================
|
||||
|
||||
rule Create_Community:
|
||||
[ Fr(~comm), Fr(~sk_comm) ]
|
||||
--[
|
||||
CommunityCreated(~comm, pk(~sk_comm))
|
||||
]->
|
||||
[
|
||||
!Community(~comm),
|
||||
!CommunitySigningKey(~comm, ~sk_comm),
|
||||
AuditHead(~comm, 'genesis')
|
||||
]
|
||||
|
||||
rule Register_Channel:
|
||||
[ !Community(comm), Fr(~chan) ]
|
||||
--[
|
||||
ChannelRegistered(~chan, comm)
|
||||
]->
|
||||
[
|
||||
!ChannelCommunity(~chan, comm),
|
||||
Out(~chan)
|
||||
]
|
||||
|
||||
rule Register_Client:
|
||||
[ Fr(~sk_client) ]
|
||||
--[
|
||||
ClientRegistered(pk(~sk_client))
|
||||
]->
|
||||
[
|
||||
!ClientPublic(pk(~sk_client)),
|
||||
!ClientSecret(pk(~sk_client), ~sk_client),
|
||||
Out(pk(~sk_client))
|
||||
]
|
||||
|
||||
rule Compromise_Client_Key:
|
||||
[ !ClientSecret(client, sk) ]
|
||||
--[
|
||||
ClientKeyCompromised(client)
|
||||
]->
|
||||
[ Out(sk) ]
|
||||
|
||||
// ============================================================================
|
||||
// NIP-98 minting
|
||||
// ============================================================================
|
||||
|
||||
// A single wire constructor models all mint requests. The requested channel set
|
||||
// is bounded to two slots for model finiteness; a one-channel mint is represented
|
||||
// as (chanA = chanB). This avoids proving S2 only for a special "multi" shape:
|
||||
// acceptance vs rejection is forced solely by server-side resolution of the
|
||||
// requested channels, not by which constructor the client chose.
|
||||
//
|
||||
// The client signs a kind:27235 event binding URL, method, payload hash,
|
||||
// freshness bucket, and the full requested channel set. Freshness is abstracted
|
||||
// as a relay-accepted time bucket; exact ±60s wall-clock arithmetic is a prose
|
||||
// / implementation axiom under P3.
|
||||
rule Client_Sends_NIP98_Mint:
|
||||
[ !ClientSecret(client, sk),
|
||||
!ChannelCommunity(chanA, commA),
|
||||
!ChannelCommunity(chanB, commB),
|
||||
Fr(~url), Fr(~body), Fr(~time) ]
|
||||
--[
|
||||
NIP98MintRequested(h(< client, ~url, h(~body), ~time, chanA, chanB >),
|
||||
client, chanA, commA, chanB, commB)
|
||||
]->
|
||||
[
|
||||
Out(
|
||||
< 'nip98_mint',
|
||||
client,
|
||||
~url,
|
||||
'POST',
|
||||
h(~body),
|
||||
~time,
|
||||
chanA,
|
||||
chanB,
|
||||
sign(< 'kind27235', client, ~url, 'POST', h(~body), ~time, chanA, chanB >, sk)
|
||||
>
|
||||
)
|
||||
]
|
||||
|
||||
// Successful mint: both requested channels resolve to the same community. The
|
||||
// stamped community is a fact on the token term (`!Token(tok, client, comm)`) and
|
||||
// each requested channel is recorded as resolving to that stamp.
|
||||
rule Relay_Mints_Token_All_Channels_Same_Community:
|
||||
[ In(
|
||||
< 'nip98_mint',
|
||||
client,
|
||||
url,
|
||||
'POST',
|
||||
payload_hash,
|
||||
time,
|
||||
chanA,
|
||||
chanB,
|
||||
sig
|
||||
>
|
||||
),
|
||||
!ClientPublic(client),
|
||||
!ChannelCommunity(chanA, comm),
|
||||
!ChannelCommunity(chanB, comm),
|
||||
Fr(~tok)
|
||||
]
|
||||
--[
|
||||
Eq(verify(sig, < 'kind27235', client, url, 'POST', payload_hash, time, chanA, chanB >, client), true),
|
||||
AllResolveSame(h(< client, url, payload_hash, time, chanA, chanB >), comm, chanA, chanB),
|
||||
NIP98Accepted(h(< client, url, payload_hash, time, chanA, chanB >), client, comm, chanA),
|
||||
NIP98Accepted(h(< client, url, payload_hash, time, chanA, chanB >), client, comm, chanB),
|
||||
TokenMinted(~tok, client, comm),
|
||||
TokenMintedForRequest(~tok, h(< client, url, payload_hash, time, chanA, chanB >), client, comm),
|
||||
TokenStamped(~tok, comm),
|
||||
MintChannel(~tok, chanA, comm),
|
||||
MintChannel(~tok, chanB, comm),
|
||||
RequestChannel(h(< client, url, payload_hash, time, chanA, chanB >), chanA, comm),
|
||||
RequestChannel(h(< client, url, payload_hash, time, chanA, chanB >), chanB, comm)
|
||||
]->
|
||||
[
|
||||
!Token(~tok, client, comm),
|
||||
Out(~tok)
|
||||
]
|
||||
|
||||
// Failed mint: the same wire constructor, same signed shape, but the server-side
|
||||
// resolver finds two different communities. This emits a rejection witness and
|
||||
// produces no token. S2 is therefore about resolution, not about the client
|
||||
// selecting a special "cross-community" event type.
|
||||
rule Relay_Rejects_Mint_Channels_Resolve_Differently:
|
||||
[ In(
|
||||
< 'nip98_mint',
|
||||
client,
|
||||
url,
|
||||
'POST',
|
||||
payload_hash,
|
||||
time,
|
||||
chanA,
|
||||
chanB,
|
||||
sig
|
||||
>
|
||||
),
|
||||
!ClientPublic(client),
|
||||
!ChannelCommunity(chanA, commA),
|
||||
!ChannelCommunity(chanB, commB)
|
||||
]
|
||||
--[
|
||||
Eq(verify(sig, < 'kind27235', client, url, 'POST', payload_hash, time, chanA, chanB >, client), true),
|
||||
Neq(commA, commB),
|
||||
ChannelsResolveDifferently(h(< client, url, payload_hash, time, chanA, chanB >), commA, commB, chanA, chanB),
|
||||
CrossCommunityMintRejected(h(< client, url, payload_hash, time, chanA, chanB >), client, commA, commB, chanA, chanB)
|
||||
]->
|
||||
[ ]
|
||||
|
||||
rule Leak_Token:
|
||||
[ !Token(tok, client, comm) ]
|
||||
--[
|
||||
TokenLeaked(tok, client, comm)
|
||||
]->
|
||||
[ Out(tok) ]
|
||||
|
||||
// ============================================================================
|
||||
// Token use
|
||||
// ============================================================================
|
||||
|
||||
// Token use resolves the target community server-side from the requested channel.
|
||||
// There is intentionally no client-supplied community or h-tag in this rule.
|
||||
// The connection's HOST is *also* authoritative: the rule only fires when the
|
||||
// host's bound community equals the channel's resolved community, so an A-host
|
||||
// presenting a B-channel-bearing request cannot authorize (the confused-deputy
|
||||
// fence on the host axis, mirroring the channel-less case). The combined witness
|
||||
// ChannelBearingResolved(tok, used_comm, host, host_comm) is emitted by this SAME
|
||||
// rule firing so the agreement lemma is a single-fact assertion -- no second-fact
|
||||
// lookup, so the M8 mutation falsifies in one rule instance.
|
||||
rule Use_Token:
|
||||
[ In(tok), !Token(tok, client, comm), !ChannelCommunity(chan, comm),
|
||||
!HostCommunity(host, comm) ]
|
||||
--[
|
||||
ActionAuthorized(tok, client, comm, chan),
|
||||
HostBoundFor(host, comm),
|
||||
ChannelBearingResolved(tok, comm, host, comm),
|
||||
TokenUsedForCommunity(tok, comm)
|
||||
]->
|
||||
[ ]
|
||||
|
||||
// Non-vacuity mutation M8 (DO NOT ENABLE in the real model): the relay authorizes
|
||||
// a channel-bearing op from the channel mapping while ignoring the host binding,
|
||||
// so an A-host can drive a B-channel op (host/channel disagreement accepted).
|
||||
//
|
||||
// rule MUTATION_Use_Token_Ignore_Host:
|
||||
// [ In(tok), !Token(tok, client, comm), !ChannelCommunity(chan, comm),
|
||||
// !HostCommunity(host, host_comm) ]
|
||||
// --[
|
||||
// Neq(comm, host_comm),
|
||||
// ActionAuthorized(tok, client, comm, chan),
|
||||
// HostBoundFor(host, host_comm),
|
||||
// ChannelBearingResolved(tok, comm, host, host_comm),
|
||||
// TokenUsedForCommunity(tok, comm)
|
||||
// ]->
|
||||
// [ ]
|
||||
//
|
||||
// Expected mutation result: `channelbearing_use_agrees_with_host` goes red. The
|
||||
// lemma reads a SINGLE ChannelBearingResolved(tok, used, host, host_comm) fact and
|
||||
// asserts used = host_comm; the mutation emits used = comm, host_comm under
|
||||
// Neq(comm, host_comm), so the counterexample is one rule instance. Confirmed:
|
||||
// falsified with a 14-step trace on Tamarin 1.12.0 / Maude 3.5.1.
|
||||
|
||||
// Non-vacuity mutation for S1 (DO NOT ENABLE in the real model): this is the
|
||||
// tempting confused-deputy bug where the relay authorizes from a client-supplied
|
||||
// claimed community / h-tag rather than from `!ChannelCommunity(chan, comm)`.
|
||||
//
|
||||
// rule MUTATION_Use_Token_Claimed_Community:
|
||||
// [ In(< tok, claimed_comm >), !Token(tok, client, minted_comm) ]
|
||||
// --[
|
||||
// Neq(minted_comm, claimed_comm),
|
||||
// ActionAuthorized(tok, client, claimed_comm, 'attacker-chosen-channel'),
|
||||
// TokenUsedForCommunity(tok, claimed_comm)
|
||||
// ]->
|
||||
// [ ]
|
||||
//
|
||||
// Expected mutation result: `token_confinement` goes red with a trace containing
|
||||
// TokenMinted(tok, client, minted_comm) and ActionAuthorized(..., claimed_comm,
|
||||
// ...) under Neq(minted_comm, claimed_comm). Confirmed by uncommenting this
|
||||
// rule and running `tamarin-prover --prove=token_confinement`: falsified with a
|
||||
// 15-step trace on Tamarin 1.12.0 / Maude 3.5.1.
|
||||
|
||||
// Probe rule: the adversary can try to use a token against a channel in another
|
||||
// community; the real model records the attempt but does not authorize it.
|
||||
rule Probe_Cross_Community_Token_Use:
|
||||
[ In(tok), !Token(tok, client, minted_comm), !ChannelCommunity(chan, resolved_comm) ]
|
||||
--[
|
||||
Neq(minted_comm, resolved_comm),
|
||||
CrossCommunityUseAttempt(tok, client, minted_comm, resolved_comm, chan)
|
||||
]->
|
||||
[ ]
|
||||
|
||||
// ============================================================================
|
||||
// Host -> community binding (P-RESOLVE-HOST) and channel-less token use
|
||||
// ============================================================================
|
||||
//
|
||||
// Channel-less operations (kind:0 profiles, 1059 DMs, 30023/30174/30315/30078,
|
||||
// lists) carry no h tag, so the community cannot be resolved from a channel.
|
||||
// Per Tyler's ruling, the connection's HOST is authoritative for the community,
|
||||
// exactly as a relay URL is authoritative for a relay today, lifted one level up.
|
||||
// A host binds to exactly one community; an unmapped host has no binding and so
|
||||
// no channel-less op can resolve (fail-closed -- modeled by the absence of a
|
||||
// !HostCommunity fact, so Use_Token_ChannelLess simply cannot fire).
|
||||
|
||||
rule Bind_Host:
|
||||
[ !Community(comm), Fr(~host) ]
|
||||
--[
|
||||
HostBound(~host, comm)
|
||||
]->
|
||||
[
|
||||
!HostCommunity(~host, comm),
|
||||
Out(~host)
|
||||
]
|
||||
|
||||
// Channel-less token use. The target community is resolved server-side from the
|
||||
// connection's host, NOT from a client-supplied community/h tag and NOT from the
|
||||
// token's stamp. The token must AGREE with the host-derived community: the rule
|
||||
// only fires when !Token(tok, client, comm) and !HostCommunity(host, comm) share
|
||||
// the same comm. Host wins; a token stamped for a different community cannot
|
||||
// authorize here (see Probe_Host_Token_Mismatch). This is the confused-deputy
|
||||
// fence (I2) lifted from channel to host. The HostBoundFor action witnesses the
|
||||
// host's binding at the authorization point so the confinement lemma can join on
|
||||
// the (single-source) host binding rather than reconstructing adversary state.
|
||||
rule Use_Token_ChannelLess:
|
||||
[ In(tok), !Token(tok, client, comm), !HostCommunity(host, comm) ]
|
||||
--[
|
||||
ChannelLessAuthorized(tok, client, comm, host),
|
||||
HostBoundFor(host, comm),
|
||||
// Single combined witness: the community actually used (1st arg) alongside
|
||||
// the host's resolved community (3rd arg), emitted by the SAME rule firing.
|
||||
// In the real rule both are `comm` (host wins), so the confinement lemma is
|
||||
// a single-fact assertion -- no second-fact lookup, no source ambiguity, so
|
||||
// the mutation that breaks the equality falsifies in one rule instance.
|
||||
ChannelLessResolved(tok, comm, host, comm),
|
||||
TokenUsedForCommunity(tok, comm)
|
||||
]->
|
||||
[ ]
|
||||
|
||||
// Non-vacuity mutation for S1-host (DO NOT ENABLE in the real model): the relay
|
||||
// authorizes a channel-less op from the token's stamp while ignoring the host
|
||||
// binding, so a B-stamped token authorizes on an A-host.
|
||||
//
|
||||
// rule MUTATION_Use_Token_ChannelLess_Ignore_Host:
|
||||
// [ In(tok), !Token(tok, client, minted_comm), !HostCommunity(host, host_comm) ]
|
||||
// --[
|
||||
// Neq(minted_comm, host_comm),
|
||||
// ChannelLessAuthorized(tok, client, minted_comm, host),
|
||||
// HostBoundFor(host, host_comm),
|
||||
// ChannelLessResolved(tok, minted_comm, host, host_comm),
|
||||
// TokenUsedForCommunity(tok, minted_comm)
|
||||
// ]->
|
||||
// [ ]
|
||||
//
|
||||
// Expected mutation result: `channelless_use_confined_to_host_community` goes red.
|
||||
// The confinement lemma reads a SINGLE ChannelLessResolved(tok, used, host,
|
||||
// host_comm) fact and asserts used = host_comm; the mutation emits that fact with
|
||||
// used = minted_comm, host_comm = host_comm under Neq(minted_comm, host_comm), so
|
||||
// the counterexample is one rule instance with no second-fact lookup or adversary
|
||||
// reconstruction. Confirmed: falsified fast on Tamarin 1.12.0.
|
||||
|
||||
// Probe rule: the adversary presents a token stamped for one community over a
|
||||
// connection whose host is bound to a different community. The real model records
|
||||
// the attempt but does not authorize it (host wins / token must agree with host).
|
||||
rule Probe_Host_Token_Mismatch:
|
||||
[ In(tok), !Token(tok, client, minted_comm), !HostCommunity(host, host_comm) ]
|
||||
--[
|
||||
Neq(minted_comm, host_comm),
|
||||
HostTokenMismatchAttempt(tok, client, minted_comm, host_comm, host)
|
||||
]->
|
||||
[ ]
|
||||
|
||||
|
||||
// Open-community AUTH auto-registration. A community with no NIP-43 member
|
||||
// pubkey allowlist admits any authenticated npub, but still only into the
|
||||
// community resolved from the connection host. This is a separate admission
|
||||
// source from NIP-43 member-list signing: NIP-43 admissions emit
|
||||
// `MemberAdmitted`; open AUTH emits `OpenCommunityAutoRegistered`. Both mint the
|
||||
// same downstream `!Admitted(pk, comm)` fact, so later read/write checks stay
|
||||
// literal admission checks rather than read-path carve-outs.
|
||||
rule Mark_Open_Community:
|
||||
[ !Community(comm) ]
|
||||
--[
|
||||
OpenCommunityEnabled(comm)
|
||||
]->
|
||||
[ !OpenCommunity(comm) ]
|
||||
|
||||
rule Authenticate_To_Open_Community:
|
||||
[ !ClientPublic(pk), !HostCommunity(host, comm), !OpenCommunity(comm) ]
|
||||
--[
|
||||
OpenCommunityAutoRegistered(pk, comm, host),
|
||||
HostBoundFor(host, comm),
|
||||
OpenRegistrationResolved(pk, comm, host, comm)
|
||||
]->
|
||||
[ !Admitted(pk, comm) ]
|
||||
|
||||
// ============================================================================
|
||||
// Per-community signing keys
|
||||
// ============================================================================
|
||||
//
|
||||
// NIP-29 grounding: relay-signed `39000`/`39001`/`39002` discovery/system events
|
||||
// are community-scoped even when group ids collide. The signed preimage commits
|
||||
// to (event kind, community id, group id, payload), so a B-key-signed metadata,
|
||||
// admin-list, or member-list event cannot be replayed as an A event.
|
||||
|
||||
rule Community_Signs_NIP29_System_Event:
|
||||
[ !CommunitySigningKey(comm, sk), Fr(~group), Fr(~payload) ]
|
||||
--[
|
||||
SystemEventSigned(comm, '39000', ~group, h(~payload)),
|
||||
SystemEventSigned(comm, '39001', ~group, h(~payload)),
|
||||
SystemEventSigned(comm, '39002', ~group, h(~payload))
|
||||
]->
|
||||
[
|
||||
Out(< 'system_event', '39000', comm, ~group, h(~payload),
|
||||
sign(< 'system_event', '39000', comm, ~group, h(~payload) >, sk) >),
|
||||
Out(< 'system_event', '39001', comm, ~group, h(~payload),
|
||||
sign(< 'system_event', '39001', comm, ~group, h(~payload) >, sk) >),
|
||||
Out(< 'system_event', '39002', comm, ~group, h(~payload),
|
||||
sign(< 'system_event', '39002', comm, ~group, h(~payload) >, sk) >)
|
||||
]
|
||||
|
||||
rule Relay_Accepts_System_Event:
|
||||
[ In(< 'system_event', kind, comm, group, msg,
|
||||
sign(< 'system_event', kind, comm, group, msg >, sk) >),
|
||||
!CommunitySigningKey(comm, sk)
|
||||
]
|
||||
--[
|
||||
SystemEventAccepted(comm, kind, group, msg)
|
||||
]->
|
||||
[ ]
|
||||
|
||||
rule Compromise_Community_Signing_Key:
|
||||
[ !CommunitySigningKey(comm, sk) ]
|
||||
--[
|
||||
CommunityKeyCompromised(comm)
|
||||
]->
|
||||
[ Out(sk) ]
|
||||
|
||||
// ============================================================================
|
||||
// NIP-43 community member-npub allowlist admission
|
||||
// ============================================================================
|
||||
//
|
||||
// NIP-43 grounding: a relay-signed member-list event names pubkeys that are
|
||||
// admitted to a community. The signed preimage commits to (community id,
|
||||
// group id, pubkey), so a B-key-signed member-list event cannot mint an
|
||||
// admission into community A even under group-id collision. Acceptance is
|
||||
// gated by the same key-binding discipline as Relay_Accepts_System_Event:
|
||||
// the signature is verified against `!CommunitySigningKey(comm, sk)`, which
|
||||
// binds `comm` to the resolved community at acceptance time, never the
|
||||
// claimed one (same confused-deputy discipline as Use_Token's host fence).
|
||||
//
|
||||
// `!Admitted(pk, comm)` is the persistent fact a downstream layer would
|
||||
// consult to decide whether a pubkey is admitted to a community; the TLA+
|
||||
// counterpart is `admittedMembers ⊆ (Communities × Actors)` populated by an
|
||||
// `AdmitMember(w)` action. The cross-lane claim is one property witnessed in
|
||||
// two model worlds: TLA+ proves the in-relay scoping (a B-admitted actor
|
||||
// cannot act in A); Tamarin proves the admission event itself is
|
||||
// per-community unforgeable (B's key cannot mint an admission into A).
|
||||
|
||||
rule Community_Signs_NIP43_MemberList:
|
||||
[ !CommunitySigningKey(comm, sk), Fr(~group), !ClientPublic(pk) ]
|
||||
--[
|
||||
MemberListSigned(comm, ~group, pk)
|
||||
]->
|
||||
[
|
||||
Out(< 'member_list', comm, ~group, pk,
|
||||
sign(< 'member_list', comm, ~group, pk >, sk) >)
|
||||
]
|
||||
|
||||
rule Relay_Accepts_NIP43_MemberList:
|
||||
[ In(< 'member_list', comm, group, pk,
|
||||
sign(< 'member_list', comm, group, pk >, sk) >),
|
||||
!CommunitySigningKey(comm, sk)
|
||||
]
|
||||
--[
|
||||
MemberAdmitted(pk, comm)
|
||||
]->
|
||||
[ !Admitted(pk, comm) ]
|
||||
|
||||
// MUTATION_Admit_Ignore_Community (commented red witness):
|
||||
// Re-bind the admission community to a fresh variable so a B-signed
|
||||
// member-list event mints `!Admitted(pk, ~other_comm)` for a community
|
||||
// whose key did not sign it. This is the exact dual of
|
||||
// `MUTATION_Use_Token_Ignore_Host` (213-225): the rule fires with
|
||||
// `Neq(comm, ~other_comm)` and emits an admission into a community whose
|
||||
// signing key never authorized the event. Toggling this rule on (and
|
||||
// commenting out `Relay_Accepts_NIP43_MemberList` above) falsifies
|
||||
// `nip43_admission_confined_to_signing_community` below: a fresh
|
||||
// `~other_comm` cannot have either signed the list (different community)
|
||||
// or had its key compromised in a way that authorized this admission, so
|
||||
// the lemma's right-hand disjunction is unsatisfiable.
|
||||
//
|
||||
// rule MUTATION_Admit_Ignore_Community:
|
||||
// [ In(< 'member_list', comm, group, pk,
|
||||
// sign(< 'member_list', comm, group, pk >, sk) >),
|
||||
// !CommunitySigningKey(comm, sk),
|
||||
// Fr(~other_comm)
|
||||
// ]
|
||||
// --[
|
||||
// Neq(comm, ~other_comm),
|
||||
// MemberAdmitted(pk, ~other_comm)
|
||||
// ]->
|
||||
// [ !Admitted(pk, ~other_comm) ]
|
||||
//
|
||||
// Expected mutation result: `nip43_admission_confined_to_signing_community`
|
||||
// goes red.
|
||||
|
||||
// ============================================================================
|
||||
// Independent per-community audit chains
|
||||
// ============================================================================
|
||||
//
|
||||
// Target shape, not today's implementation: current `buzz-audit` has one global
|
||||
// chain (`buzz-audit/src/service.rs` reads the latest global hash). Multi-tenant
|
||||
// safety requires N independent community-labeled heads so the spec's
|
||||
// Implementation Correspondence section can track replacing the global chain.
|
||||
|
||||
rule Append_Audit:
|
||||
[ AuditHead(comm, prev), Fr(~seq), Fr(~entry) ]
|
||||
--[
|
||||
AuditEntryCreated(comm, ~seq, prev, h(< 'audit', comm, ~seq, prev, ~entry >)),
|
||||
AuditAppended(comm, prev, h(< 'audit', comm, ~seq, prev, ~entry >)),
|
||||
AuditHeadAdvanced(comm, prev, h(< 'audit', comm, ~seq, prev, ~entry >))
|
||||
]->
|
||||
[
|
||||
AuditHead(comm, h(< 'audit', comm, ~seq, prev, ~entry >)),
|
||||
Out(h(< 'audit', comm, ~seq, prev, ~entry >))
|
||||
]
|
||||
|
||||
rule Probe_Audit_Cross_Community_Splice:
|
||||
[ AuditHead(commA, prevA), AuditHead(commB, prevB), Fr(~seq), Fr(~entry) ]
|
||||
--[
|
||||
Neq(commA, commB),
|
||||
CrossCommunityAuditSpliceAttempt(commA, commB, prevA, prevB, h(< 'audit', commA, ~seq, prevB, ~entry >))
|
||||
]->
|
||||
[
|
||||
// Restore both heads unchanged: the probe models an *attempt* that does
|
||||
// not advance either chain. Without restoring, a successful probe firing
|
||||
// would erase both heads from the trace, preventing any further audit
|
||||
// appends in the same execution. Soundness of
|
||||
// `cross_community_audit_splice_attempt_is_not_append` does not depend
|
||||
// on this (no rule emits `AuditAppended` from this attempt), but
|
||||
// tightening the model so the attempt does not consume the chains makes
|
||||
// the trace shape match reality.
|
||||
AuditHead(commA, prevA),
|
||||
AuditHead(commB, prevB)
|
||||
]
|
||||
|
||||
// ============================================================================
|
||||
// Draft security lemmas
|
||||
// ============================================================================
|
||||
|
||||
lemma executable_core_flow:
|
||||
exists-trace
|
||||
"Ex tok client comm chan #i #j.
|
||||
TokenMinted(tok, client, comm) @ i
|
||||
& ActionAuthorized(tok, client, comm, chan) @ j
|
||||
& #i < #j"
|
||||
|
||||
lemma executable_cross_community_mint_rejection:
|
||||
exists-trace
|
||||
"Ex req client commA commB chanA chanB #i.
|
||||
CrossCommunityMintRejected(req, client, commA, commB, chanA, chanB) @ i"
|
||||
|
||||
// S1: token use is confined to the token's stamped community. This remains true
|
||||
// even when `Leak_Token` makes the bearer token known to the adversary.
|
||||
lemma token_confinement:
|
||||
"All tok client minted_comm used_comm chan #i #j.
|
||||
TokenMinted(tok, client, minted_comm) @ i
|
||||
& ActionAuthorized(tok, client, used_comm, chan) @ j
|
||||
==> minted_comm = used_comm"
|
||||
|
||||
lemma leaked_token_blast_radius_contained:
|
||||
"All tok client minted_comm used_comm chan #i #j.
|
||||
TokenLeaked(tok, client, minted_comm) @ i
|
||||
& ActionAuthorized(tok, client, used_comm, chan) @ j
|
||||
==> minted_comm = used_comm"
|
||||
|
||||
lemma cross_community_use_attempts_are_not_authorized:
|
||||
"All tok client minted_comm resolved_comm chan #i.
|
||||
CrossCommunityUseAttempt(tok, client, minted_comm, resolved_comm, chan) @ i
|
||||
==> not (Ex #j. ActionAuthorized(tok, client, resolved_comm, chan) @ j)"
|
||||
|
||||
// S1-host: a channel-less authorization is confined to the community bound to the
|
||||
// connection's HOST. The lemma reads a single ChannelLessResolved(tok, used_comm,
|
||||
// host, host_comm) fact -- emitted by the authorizing rule and carrying both the
|
||||
// community actually used and the host's resolved community -- and asserts they
|
||||
// are equal. A single-fact assertion means a counterexample is one rule instance,
|
||||
// not a multi-fact join or adversary reconstruction. Host wins over the token's
|
||||
// stamp: enabling MUTATION_Use_Token_ChannelLess_Ignore_Host falsifies this fast.
|
||||
lemma channelless_use_confined_to_host_community:
|
||||
"All tok used_comm host host_comm #i.
|
||||
ChannelLessResolved(tok, used_comm, host, host_comm) @ i
|
||||
==> used_comm = host_comm"
|
||||
|
||||
// S1-host (channel-bearing): a channel-BEARING authorization is confined to the
|
||||
// community bound to the connection's HOST -- the host axis of the confused-deputy
|
||||
// fence. Today the relay resolves a channel-bearing op's community from the h tag
|
||||
// (the channel mapping) alone; this lemma proves that the host must ALSO agree, so
|
||||
// an A-host presenting a B-channel-bearing request cannot authorize as B. Like the
|
||||
// channel-less case it reads a single ChannelBearingResolved(tok, used_comm, host,
|
||||
// host_comm) fact, so a counterexample is one rule instance. Enabling
|
||||
// MUTATION_Use_Token_Ignore_Host (which accepts host/channel disagreement)
|
||||
// falsifies this fast.
|
||||
lemma channelbearing_use_agrees_with_host:
|
||||
"All tok used_comm host host_comm #i.
|
||||
ChannelBearingResolved(tok, used_comm, host, host_comm) @ i
|
||||
==> used_comm = host_comm"
|
||||
|
||||
// The token presented for a channel-less op must agree with the host-derived
|
||||
// community: the real rule only fires when the token's stamp equals the host's
|
||||
// community, so any recorded channel-less authorization carries a token whose
|
||||
// mint stamp matches the used community.
|
||||
lemma channelless_token_agrees_with_host:
|
||||
"All tok client used_comm host minted_comm #i #j.
|
||||
ChannelLessAuthorized(tok, client, used_comm, host) @ i
|
||||
& TokenMinted(tok, client, minted_comm) @ j
|
||||
==> used_comm = minted_comm"
|
||||
|
||||
// A token stamped for one community presented over a host bound to a different
|
||||
// community (the host/token mismatch) is never channel-less authorized for the
|
||||
// token's stamped community over that host.
|
||||
lemma host_token_mismatch_not_authorized:
|
||||
"All tok client minted_comm host_comm host #i.
|
||||
HostTokenMismatchAttempt(tok, client, minted_comm, host_comm, host) @ i
|
||||
==> not (Ex #j. ChannelLessAuthorized(tok, client, minted_comm, host) @ j)"
|
||||
|
||||
// Open-community auto-registration is host-confined: the registered community is
|
||||
// exactly the community bound to the connection host. There is no client-supplied
|
||||
// community selector in the rule.
|
||||
lemma open_auth_registration_confined_to_host_community:
|
||||
"All pk registered_comm host host_comm #i.
|
||||
OpenRegistrationResolved(pk, registered_comm, host, host_comm) @ i
|
||||
==> registered_comm = host_comm"
|
||||
|
||||
// S2: every minted token has exactly one stamped community, and every requested
|
||||
// channel recorded for that mint resolved to that stamp.
|
||||
lemma minted_token_channels_match_stamp:
|
||||
"All tok client comm chan chan_comm #i #j.
|
||||
TokenMinted(tok, client, comm) @ i
|
||||
& MintChannel(tok, chan, chan_comm) @ j
|
||||
==> comm = chan_comm"
|
||||
|
||||
lemma minted_request_channels_match_stamp:
|
||||
"All tok req client comm chan chan_comm #i #j #k.
|
||||
TokenMintedForRequest(tok, req, client, comm) @ i
|
||||
& RequestChannel(req, chan, chan_comm) @ j
|
||||
& TokenStamped(tok, comm) @ k
|
||||
==> comm = chan_comm"
|
||||
|
||||
lemma token_stamp_matches_mint:
|
||||
"All tok client comm stamp #i #j.
|
||||
TokenMinted(tok, client, comm) @ i
|
||||
& TokenStamped(tok, stamp) @ j
|
||||
==> comm = stamp"
|
||||
|
||||
lemma cross_community_mint_yields_no_token_for_that_request:
|
||||
"All req client commA commB chanA chanB #i.
|
||||
CrossCommunityMintRejected(req, client, commA, commB, chanA, chanB) @ i
|
||||
==> not (Ex tok comm #j. TokenMintedForRequest(tok, req, client, comm) @ j)"
|
||||
|
||||
// S3 shape: accepting an event for community A requires A's signing key, unless
|
||||
// A's signing key has been compromised. Compromise of another community's key is
|
||||
// not sufficient because the signed preimage includes the community id.
|
||||
lemma system_event_acceptance_requires_same_community_key_or_compromise:
|
||||
"All comm kind group msg #i.
|
||||
SystemEventAccepted(comm, kind, group, msg) @ i
|
||||
==> (Ex #j. SystemEventSigned(comm, kind, group, msg) @ j & #j < #i)
|
||||
| (Ex #k. CommunityKeyCompromised(comm) @ k & #k < #i)"
|
||||
|
||||
lemma other_community_key_compromise_does_not_authorize:
|
||||
"All commA commB kind group msg #i #j #k.
|
||||
CommunityKeyCompromised(commB) @ i
|
||||
& SystemEventAccepted(commA, kind, group, msg) @ j
|
||||
& Neq(commA, commB) @ k
|
||||
==> (Ex #l. SystemEventSigned(commA, kind, group, msg) @ l & #l < #j)
|
||||
| (Ex #m. CommunityKeyCompromised(commA) @ m & #m < #j)"
|
||||
|
||||
// S5 shape: every NIP-43 admission of `pk` into community A requires either
|
||||
// (a) a `MemberListSigned(A, _, pk)` event preceding the admission, or
|
||||
// (b) A's signing key was compromised before the admission. Since acceptance
|
||||
// in `Relay_Accepts_NIP43_MemberList` re-verifies the signature against
|
||||
// `!CommunitySigningKey(comm, sk)` (binding `comm` at acceptance, not at
|
||||
// claim), the admission community is forced to be the same community whose
|
||||
// key signed the list event. This is the load-bearing cross-community claim
|
||||
// for community-scoped member-npub allowlists: B's key cannot mint an
|
||||
// admission into A.
|
||||
lemma nip43_admission_confined_to_signing_community:
|
||||
"All pk comm #i.
|
||||
MemberAdmitted(pk, comm) @ i
|
||||
==> (Ex group #j. MemberListSigned(comm, group, pk) @ j & #j < #i)
|
||||
| (Ex #k. CommunityKeyCompromised(comm) @ k & #k < #i)"
|
||||
|
||||
// Sibling to `other_community_key_compromise_does_not_authorize`: compromise
|
||||
// of community B's signing key never suffices to admit a pubkey into a
|
||||
// different community A. The signed preimage of a member-list event binds
|
||||
// the community id, so B's compromise yields no admission for A — A must
|
||||
// either have signed the list for `pk` itself or had its own key
|
||||
// compromised.
|
||||
lemma other_community_key_compromise_does_not_admit:
|
||||
"All commA commB pk #i #j #k.
|
||||
CommunityKeyCompromised(commB) @ i
|
||||
& MemberAdmitted(pk, commA) @ j
|
||||
& Neq(commA, commB) @ k
|
||||
==> (Ex group #l. MemberListSigned(commA, group, pk) @ l & #l < #j)
|
||||
| (Ex #m. CommunityKeyCompromised(commA) @ m & #m < #j)"
|
||||
|
||||
// S4 shape: every audit append advances a head for the same community and the
|
||||
// next hash binds that community id, so another community's head cannot be used
|
||||
// as a splice without changing the hash/preimage.
|
||||
lemma audit_append_advances_same_community_head:
|
||||
"All comm prev next #i.
|
||||
AuditAppended(comm, prev, next) @ i
|
||||
==> AuditHeadAdvanced(comm, prev, next) @ i"
|
||||
|
||||
lemma cross_community_audit_splice_attempt_is_not_append:
|
||||
"All commA commB prevA prevB forged #i.
|
||||
CrossCommunityAuditSpliceAttempt(commA, commB, prevA, prevB, forged) @ i
|
||||
==> not (Ex #j. AuditAppended(commA, prevB, forged) @ j)"
|
||||
|
||||
// Reachability / anti-vacuity probes.
|
||||
lemma executable_token_leak:
|
||||
exists-trace
|
||||
"Ex tok client comm #i. TokenLeaked(tok, client, comm) @ i"
|
||||
|
||||
lemma leaked_token_can_authorize_within_its_community:
|
||||
exists-trace
|
||||
"Ex tok client comm chan #i #j.
|
||||
TokenLeaked(tok, client, comm) @ i
|
||||
& ActionAuthorized(tok, client, comm, chan) @ j"
|
||||
|
||||
lemma executable_system_event_acceptance:
|
||||
exists-trace
|
||||
"Ex comm kind group msg #i. SystemEventAccepted(comm, kind, group, msg) @ i"
|
||||
|
||||
lemma executable_other_key_compromise_plus_system_accept:
|
||||
exists-trace
|
||||
"Ex commA commB kind group msg #i #j #k.
|
||||
CommunityKeyCompromised(commB) @ i
|
||||
& SystemEventAccepted(commA, kind, group, msg) @ j
|
||||
& Neq(commA, commB) @ k"
|
||||
|
||||
lemma executable_cross_community_audit_splice_attempt:
|
||||
exists-trace
|
||||
"Ex commA commB prevA prevB forged #i.
|
||||
CrossCommunityAuditSpliceAttempt(commA, commB, prevA, prevB, forged) @ i"
|
||||
|
||||
lemma executable_signing_key_compromise:
|
||||
exists-trace
|
||||
"Ex comm #i. CommunityKeyCompromised(comm) @ i"
|
||||
|
||||
lemma executable_audit_append:
|
||||
exists-trace
|
||||
"Ex comm prev next #i. AuditAppended(comm, prev, next) @ i"
|
||||
|
||||
// Host-binding reachability probes (anti-vacuity for the S1-host lemmas).
|
||||
lemma executable_host_bound:
|
||||
exists-trace
|
||||
"Ex host comm #i. HostBound(host, comm) @ i"
|
||||
|
||||
lemma executable_channelless_use:
|
||||
exists-trace
|
||||
"Ex tok client comm host #i.
|
||||
ChannelLessAuthorized(tok, client, comm, host) @ i"
|
||||
|
||||
lemma executable_host_token_mismatch_attempt:
|
||||
exists-trace
|
||||
"Ex tok client minted_comm host_comm host #i.
|
||||
HostTokenMismatchAttempt(tok, client, minted_comm, host_comm, host) @ i"
|
||||
|
||||
// Anti-vacuity probe for nip43_admission_confined_to_signing_community: there
|
||||
// must be a trace in which a member-list event is signed and accepted into
|
||||
// the admitting community, so the lemma's left-hand side is reachable.
|
||||
lemma executable_member_admitted:
|
||||
exists-trace
|
||||
"Ex pk comm #i. MemberAdmitted(pk, comm) @ i"
|
||||
|
||||
lemma executable_open_auth_registration:
|
||||
exists-trace
|
||||
"Ex pk comm host #i. OpenCommunityAutoRegistered(pk, comm, host) @ i"
|
||||
|
||||
end
|
||||
@@ -0,0 +1,32 @@
|
||||
\* TLC model-check config for the draft MultiTenantRelay model.
|
||||
\* Run:
|
||||
\* java -cp ~/.buzz/.scratch/tla2tools.jar tlc2.TLC -config MultiTenantRelay.cfg MultiTenantRelay.tla
|
||||
SPECIFICATION Spec
|
||||
|
||||
CONSTANTS
|
||||
Communities = {commA, commB}
|
||||
Channels = {chanA1, chanA2, chanB1, chanB2, chanFresh}
|
||||
Hosts = {hostA, hostB, hostBad}
|
||||
Actors = {alice}
|
||||
Workers = {relay1}
|
||||
MsgIds = {msg1}
|
||||
AuditVals = {audit0, audit1}
|
||||
CommA = commA
|
||||
CommB = commB
|
||||
ChanA1 = chanA1
|
||||
ChanA2 = chanA2
|
||||
ChanB1 = chanB1
|
||||
ChanB2 = chanB2
|
||||
ChanFresh = chanFresh
|
||||
HostA = hostA
|
||||
HostB = hostB
|
||||
HostBad = hostBad
|
||||
NoChannel = noChannel
|
||||
NoCommunity = noCommunity
|
||||
OpenCommunities = {commA}
|
||||
SanitizedErrors = {"auth-required", "restricted", "invalid", "duplicate", "pow", "rate-limited", "blocked", "error", "frame-too-large"}
|
||||
|
||||
INVARIANT Safety
|
||||
CONSTRAINT BoundedObservations
|
||||
CONSTRAINT BoundedWitnesses
|
||||
SYMMETRY Symmetry
|
||||
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user