Break the ceremony.
EMILIA is the authorization-receipt layer for irreversible AI-agent actions: no valid human-signed receipt, no execution — and afterward, anyone can verify who approved exactly what, without trusting us. This page is where you try to prove that wrong.
We claim EMILIA’s authorization ceremony cannot be replayed, forged, self-approved, or reversed — and we proved it with a model checker. Don’t take our word for it. The protocol is open. The receipts are public. Try to break it.
Safety infrastructure earns trust by surviving attack in the open. Every confirmed break — and its fix — gets published here, with credit.
What counts as a break
What a receipt proves — and what it doesn’t
The honesty is the credential. Here is exactly where the guarantee starts and stops.
- ✓A named human — or a quorum of distinct humans — signed THIS exact action (amount, payee, target), not a session and not a scope.
- ✓Anyone can verify it offline, with no account and no trust in the operator or in EMILIA.
- ✓Tamper with one byte of the authorized action and verification fails.
- ✓The authorization is consumable exactly once — replays are rejected.
- ✓Missing, invalid, expired, or wrong-approver → the action does not proceed. Fail-closed by default.
- —That the decision was correct or wise. EP proves authorization, not judgment.
- —Real-world identity beyond the enrollment layer. A receipt proves the enrolled key signed; identity proofing is a separate, stated layer.
- —The negative of an absence you were never handed. One-time-use and revocation freshness are server-state — ask the operator for the consumption record and any signed revocation (itself offline-verifiable).
Attacks we reject — and what backs each claim
Run the negative cases yourself: npx @emilia-protocol/crash-test issues a genuine receipt, verifies it offline, then shows the forged copy being rejected.
A real authority-binding bug, found in red-team and fixed
In an adversarial pass we found that a leaked receipt_id could let another authenticated actor attach their own signoff flow to someone else’s receipt and self-approve it. The cryptography was sound; the authority-binding glue was not.
We closed it by binding signoff requests to the receipt creator and approvals to the intended approver — now row four of the matrix above. We publish this on purpose: the danger zone for systems like this is authority binding and deployment semantics, not the math, and finding it in the open is the point of this page.
Anyone can copy a schema. They cannot copy a security case by changing the logo.
EMILIA’s differentiation is not proprietary cryptography. It is a composed, machine-rerunnable argument that the whole path holds together: challenge, canonical action, human ceremony, issuer and authority pins, revocation, one-time consumption, and execution.
↓ canonical action
↓ human ceremony
↓ issuer + authority
↓ revocation
↓ consumption
↓ execution
Tamarin tests this as one symbolic protocol under a Dolev-Yao attacker with full network control, rather than assuming separately checked pieces compose safely.
execution_requires_full_compositionVERIFIED · ALL TRACESExecution requires challenge, exact action, approvals, pinned authority, revocation, and consumption to compose.
no_issuer_launderingVERIFIED · ALL TRACESA presenter cannot turn its own key into an accepted issuer by relabeling the artifact.
no_cross_action_profile_or_audience_replayVERIFIED · ALL TRACESValid evidence cannot be transplanted to another action, profile, or relying party.
initiator_cannot_self_approveVERIFIED · ALL TRACESThe actor initiating an action cannot fill the human-approval seat.
strict_registry_view_is_exactVERIFIED · ALL TRACESAuthority evidence must match the exact registry checkpoint pinned by the relying party.
injective_execution_with_consumptionVERIFIED · ALL TRACESOne consumed authorization maps to at most one checked execution.
We deliberately remove controls and ask Tamarin to find the failure.
unchecked_composition_is_injectiveRemove one-time consumption and Tamarin finds a same-receipt replay.
unchecked_registry_view_is_currentRemove exact registry-view binding and Tamarin accepts a stale or equivocating authority view.
Open does not mean interchangeable.
Nothing prevents another team from implementing the open format. That is the distribution strategy. But a compatible envelope is not an equivalent system. Equivalence means reproducing the composed proof, strict verifier behavior, negative vectors, durable consumption, release evidence, and every assumption and exclusion. Each discovered failure becomes a permanent, machine-rerunnable obligation. That body of evidence compounds with every release.
Broader executable evidence: 26 TLA+ invariants · 35 Alloy facts + 32 assertions · 8,755 automated cases · 331 current conformance vectors.
Scope remains explicit: TLA+ and Alloy model bounded state and relational properties; Tamarin uses symbolic perfect cryptography and pinned-root assumptions. These are not proofs of AI behavior, WebAuthn internals, parser correctness, legal compliance, or deployment completeness.
The transparency contract
- —Every confirmed break is published here within 7 days, with the attacker’s credit (or anonymous, your call).
- —Every fix is published alongside it — the spec change, the code, and the new passing proof.
- —The running tally above (confirmed breaks) is never silently reset.
- —In scope: the authorization ceremony, the signed-receipt format, the consume gate, the verifier.
- —Out of scope: DDoS, social engineering, third-party infra (Vercel/Supabase), and anything against production tenant data.
Start swinging
The protocol, the SDK, and a public demo receipt are live now — attack those directly. Scoped challenge keys against an isolated instance open shortly; report anything you find to the address below in the meantime.
Report a break: team@emiliaprotocol.ai