Interactive demo

Financial-institution scenario

A retail bank's data lakehouse holds three tables — users_data, cards_data, transactions_data — ingested from upstream CRM, card-management, and ledger systems. Three internal departments query the lake through LLM agents. Each department has a different reason to look at the same rows, so the policy gates which columns reach each agent. Submit a plan and the WASM-compiled rewriter answers: rewrite with a projected column list, or refuse with a reason.

Cast — the three principals

Each principal is a department-scoped agent identity. The Postern gateway extracts the principal from a Biscuit token on every request and looks up the matching grants.

`CRM`

Customer Relationship Management

Runs marketing segmentation and customer-support lookups. Needs to identify a user by id/name and know their region and age for campaign targeting. Has no business reason to see cards, transactions, or PII like ssn / email.

Allowed: users_data.{id, name, region, age}

`CardOps`

Card Operations

Handles card issuance, activation, and limit changes. Needs the card-level attributes (card_id, card_type, limit, activated) but must never see the full card_number (PAN — PCI-DSS scope) and has no business with users or transactions in this scenario.

Allowed: cards_data.{card_id, card_type, limit, activated}

`FraudRisk`

Fraud & Risk Analytics

Investigates anomalous spend patterns. Needs the full transactions table to compute spend signatures and a minimum-necessary slice of users (just id + region) to bucket by geography. Does not need name/age for the model and never sees PII or PAN.

Allowed: transactions_data.{txn_id, card_id, amount, merchant, timestamp} + users_data.{id, region}

Any principal not in this list (e.g. Marketing, a contractor) falls through the fail-closed default — the rewriter returns an empty projection, never the raw rows.

1. Raw data

Synthetic samples — same schema as the Kaggle transactions-fraud-datasets. Sensitive columns are flagged like this; the policy must never release them.

`users_data`

5 rows · 6 columns

id	name	email	ssn	region	age
u_001	Alex Chen	alex.chen@example.com	123-45-6789	EU-West	34
u_002	Priya Rao	priya.rao@example.com	234-56-7891	APAC	41
u_003	Jamal Khan	jamal.khan@example.com	345-67-8912	EU-West	29
u_004	Lin Wei	lin.wei@example.com	456-78-9123	APAC	52
u_005	Sara Müller	sara.mueller@example.com	567-89-1234	EU-West	23

`cards_data`

5 rows · 6 columns

card_id	user_id	card_number	card_type	limit	activated
c_4001	u_001	4111-1111-1111-1111	credit	15000	1
c_4002	u_002	5500-0000-0000-0004	credit	8000	1
c_4003	u_003	3400-0000-0000-009	amex	25000	0
c_4004	u_004	6011-0000-0000-0004	debit	2500	1
c_4005	u_005	4111-2222-3333-4444	credit	5000	1

`transactions_data`

5 rows · 5 columns

txn_id	card_id	amount	merchant	timestamp
t_9001	c_4001	42.5	ACME Coffee	2026-05-23T08:14:00Z
t_9002	c_4002	1299	Online Electronics	2026-05-23T14:02:00Z
t_9003	c_4005	17.85	Bakery One	2026-05-24T09:31:00Z
t_9004	c_4001	540	Airline X	2026-05-24T17:11:00Z
t_9005	c_4004	8.4	Transit Pass	2026-05-25T07:02:00Z

2. Policy

Surface syntax (left) is sugar over a list of right(p, r, c) facts (right) — one fact per principal/relation/column triple.

policy.postern

# Postern policy — financial-institution demo.
# Surface syntax is sugar over the `Grant` list in
# verifier/lean/Postern.lean (namespace Demo).

grant CRM       on users_data        { id, name, region, age }
grant CardOps   on cards_data        { card_id, card_type, limit, activated }
grant FraudRisk on transactions_data { txn_id, card_id, amount, merchant, timestamp }
grant FraudRisk on users_data        { id, region }

# Anything outside these grants is implicitly denied.
# - PII (users_data.email, users_data.ssn) is never granted.
# - PAN (cards_data.card_number) is never granted.
# - users_data.user_id link is grantable but unused by these principals.

Datalog desugaring

right("CRM", "users_data", "id").
right("CRM", "users_data", "name").
right("CRM", "users_data", "region").
right("CRM", "users_data", "age").
right("CardOps", "cards_data", "card_id").
right("CardOps", "cards_data", "card_type").
right("CardOps", "cards_data", "limit").
right("CardOps", "cards_data", "activated").
right("FraudRisk", "transactions_data", "txn_id").
right("FraudRisk", "transactions_data", "card_id").
right("FraudRisk", "transactions_data", "amount").
right("FraudRisk", "transactions_data", "merchant").
right("FraudRisk", "transactions_data", "timestamp").
right("FraudRisk", "users_data", "id").
right("FraudRisk", "users_data", "region").

2b. The biscuit on the wire

On every request, biscuit_auth::datalog::World is loaded with two layers of Datalog before evaluating an allow if right($p, $r, $c) query. Pick a principal below to see the bearer block update.

Authority block gateway-loaded

Compiled from policy.postern at gateway startup and re-added via World::add_fact per request. Trusted by construction; not signed by the bearer.

right("CRM", "users_data", "id").
right("CRM", "users_data", "name").
right("CRM", "users_data", "region").
right("CRM", "users_data", "age").
right("CardOps", "cards_data", "card_id").
right("CardOps", "cards_data", "card_type").
right("CardOps", "cards_data", "limit").
right("CardOps", "cards_data", "activated").
right("FraudRisk", "transactions_data", "txn_id").
right("FraudRisk", "transactions_data", "card_id").
right("FraudRisk", "transactions_data", "amount").
right("FraudRisk", "transactions_data", "merchant").
right("FraudRisk", "transactions_data", "timestamp").
right("FraudRisk", "users_data", "id").
right("FraudRisk", "users_data", "region").

Bearer token CRM

Ed25519-signed by the issuer (the bank's IAM). Carries only the principal identity — no rights, no scope.

user("CRM").

Serialized (mock)

En0KEwoEQ1JNGAMiCQoHCAoSAxiACBIkCAASIA...

Not modelled in this artifact (paper §6 open problems): attenuation (3rd-party caveats narrowing the bearer's rights), audience (binding the token to one gateway URL), expiry (check if time($t), $t < 2026-06-01T00:00:00Z), key rotation (root-key rollover without re-issuing every bearer). The serialized blob is a mock — not a valid Ed25519-signed token — because the WASM bundle doesn't ship biscuit-auth today.

3. Try it

Pick options and submit to see the rewrite.

About this demo

The WASM binary is the column-grant rewriter (postern-core::rewrite) compiled to wasm32-unknown-unknown via wasm-pack. It mirrors the Lean reference one-for-one.
Refusal reasons surfaced: unknown relation (catalog lookup empty) and filter on forbidden column (predicate touches columns outside the principal's grants).
Plan IR uses three operators only — Scan, Project, Filter — matching the inductive defined in verifier/lean/Postern.lean.