mirror of
https://github.com/block/buzz.git
synced 2026-08-18 06:50:31 +02:00
npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67dandTyler Longwell
f2d84bd906
Stacked on #1657 (mini/community-provisioning). The operator plane (POST /operator/communities) is the first runtime surface that can mint tenancy, so it gets the same mechanized treatment as the rest of the multi-tenant model: Tamarin (docs/spec/MultiTenantAuth.spthy, new S9 section): - Rules: Register_Operator / Compromise_Operator_Key, operator-signed provision + rotate requests (NIP-98 preimage includes the payload hash h(<host, owner>) — payload binding mandatory), relay provision + converge/rotate gated on the !OperatorKey allowlist, and the UniqueHostBinding restriction importing the append-only host map. - Lemmas: provisioning_requires_operator_authorization (allowlist gate, no compromise disjunct — compromise doesn't extend the allowlist), provision_accepts_only_operator_signed_payload (payload binding), rotation_confined_to_host_community (S5/S6-style single witness), plus three exists-trace probes incl. the create-then-converge lifecycle. - Full run: all 38 lemmas verified green (Tamarin 1.12.0 / Maude 3.5.1, ~141 s). Three commented mutations confirmed red: MUTATION_Provision_Unsigned_Body (the optional-payload-tag gap from the #1657 review; 8-step trace), MUTATION_Provision_Any_Client (8 steps), MUTATION_Rotate_Ignore_Host (12 steps). TLA+ (docs/spec/MultiTenantRelay.tla, comment-only): stated assumption P-HOST-APPEND — HostCommunity stays a constant-per-segment function because the host map is append-only (ensure_configured_community's ON CONFLICT upsert never re-points a bound host), so runtime provisioning needs no TLC remodeling. SANY-checked. Prose (docs/multi-tenant-relay.md): S9 section under Authorization soundness, verification-status update (32 -> 38 lemmas, current run figures), P-HOST-APPEND conformance row (incl. the require-payload-tag and signer-checked-allowlist obligations), Mechanized Verification bullet, machine-check-hygiene classification for the new lemmas, and a stale spthy line-reference fix (:403/:413 -> :427/:437). Co-authored-by: Tyler Longwell <tlongwell@block.xyz> Signed-off-by: Tyler Longwell <tlongwell@block.xyz>