97 Proven Theorems
Formal security proofs verified by Lean 4. Zero sorry. Zero axiom leaks. Every theorem compiles. 43 headline properties listed below; the remainder are supporting lemmas, witnesses, and structural helpers.
Proof Strength Tiers
- T1 — Structural
- Proved from model definitions alone. The property follows from how we defined the types and functions. No axioms beyond Lean's core. These are the strongest claims — if the model faithfully represents production code, the property holds unconditionally.
- T2 — Axiomatic
- Proved under explicitly stated axioms on an abstract scheme (e.g., "HMAC is key-discriminating"). The property holds if the axioms hold. Axiom satisfiability is witnessed by a concrete inhabitant that compiles.
- T3 — Model-level
- Proved at the abstract model level. The theorem is valid within the model but depends on the model faithfully capturing production behavior. The gap between model and code is noted.
AEAD — 6 properties
Models AEAD encryption with nonce-aware key/nonce discrimination, ciphertext expansion, and authenticated replay protection.
| Tier | Property | Lean theorem |
|---|---|---|
| T2 | Relay Confidentiality Decryption with any key other than the encryption key fails. | relay_cannot_extract |
| T2 | Encryption Correctness AEAD encrypt then decrypt with the same key and nonce yields the original plaintext. | aead_roundtrip |
| T1 | Session Uniqueness A successful peer insertion starts from a fresh counter. | counter_uniqueness |
| T1 | Counter Monotonicity Each new peer receives a counter strictly greater than any existing peer's. | counter_monotonicity |
| T2 | Authenticated Replay Protection A forged packet does not advance the replay window. | authenticated_replay_window |
| T2 | Replay Composition Forged packets are transparent to the system — processing one followed by an authentic packet equals processing the authentic alone. | forged_then_authentic_composition |
Auth — 19 properties
Models Ed25519 request authentication, domain separation, replay protection, registration ownership, WebSocket re-authentication, sender-DID binding, and session ticket validation.
| Tier | Property | Lean theorem |
|---|---|---|
| T2 | Request Authentication A valid signature is bound to the signer DID and full canonical message. | request_binding |
| T2 | Service Domain Separation A relay signature cannot validate as a directory message. | domain_separation |
| T2 | Body Integrity Different request bodies produce different signed digests. | body_digest_binding |
| T1 | Replay Protection (Mutating) Expired timestamps rejected regardless of signature validity. | mutating_replay_rejection |
| T1 | Nonce Replay Rejection Previously-seen nonces rejected on mutating requests. | mutating_nonce_rejection |
| T1 | Timestamp Protection (GET) Out-of-window timestamps rejected even with valid signatures. | readonly_timestamp_rejection |
| T1 | Signature Protection (GET) Invalid signatures rejected independent of timestamp. | readonly_signature_rejection |
| T1 | GET Nonce Independence Read-only validation does not consult the nonce store. | readonly_nonce_independence |
| T1 | Input Validation Malformed timestamps rejected before signature verification. | timestamp_format_strictness |
| T1 | Registration Ownership Authenticated DID must match the body's asserted DID. | registration_ownership |
| T1 | Registration Ownership (iff) Biconditional: valid iff authenticated DID equals body DID equals card DID. | registration_ownership_iff |
| T1 | Nonce Format Strictness Invalid nonce format rejected regardless of other request fields. | nonce_format_strictness |
| T1 | Timestamp Window Rejection Out-of-window timestamps rejected for all HTTP methods. | timestamp_window_rejection_all_methods |
| T2 | WS/HTTP Domain Separation HTTP signatures cannot validate as WebSocket re-auth, and vice versa. | ws_http_domain_separation |
| T1 | Sender-DID Binding Mismatched authenticated DID and sender field is rejected. | sender_did_binding |
| T2 | Ticket HMAC Binding Wrong HMAC key fails ticket validation. | ticket_hmac_binding |
| T1 | Ticket Directional Binding (from) Mismatched fromDid rejected. | ticket_from_mismatch |
| T1 | Ticket Directional Binding (to) Mismatched toDid rejected. | ticket_to_mismatch |
| T1 | Ticket Expiry Enforcement Expired tickets rejected regardless of valid HMAC. | ticket_expiry_enforcement |
Key Exchange — 3 properties
Models the Ed25519 → X25519 derivation for MITM detection, ephemeral key contribution for forward secrecy, and session state lifecycle ordering.
| Tier | Property | Lean theorem |
|---|---|---|
| T2 | MITM Detection Given a DID, there is exactly one valid X25519 key. Any mismatch reveals an attacker. | mitm_detectable |
| T2 | Forward Secrecy Changing either party's ephemeral contribution changes the upgraded session key. | forward_secrecy |
| T1 | Session State Ordering Once a session leaves Initial, it cannot be downgraded back. | no_downgrade_to_initial |
Pairing — 7 supporting lemmas
Models the Cantor pairing function used as the injective encoding for concrete AEAD and HMAC inhabitants.
| Tier | Property | Lean theorem |
|---|---|---|
| T1 | Supporting lemmas for axiom satisfiability witnesses. See Layr0/Pairing.lean. | |
Sandbox — 6 properties
Models the MeetingRoom Durable Object's agent cap, per-agent message limits, timeout, teardown finality, and graduation protocol.
| Tier | Property | Lean theorem |
|---|---|---|
| T1 | Agent Cap Enforced After two agents join, any new agent is rejected. | agent_cap_enforced |
| T1 | Message Limit Enforced Agent at or above per-agent message limit cannot send more. | message_limit_enforced |
| T1 | Teardown Finality After teardown, all joins and sends are rejected. | teardown_blocks_join |
| T1 | Timeout Enforced Room is torn down when time exceeds startTime + maxDuration. | timeout_enforced |
| T1 | Graduation Requires Mutual Proceed Room completes only when all agents have their proceeded flag set. | graduation_requires_all_proceeded |
| T1 | Bail Prevents Graduation After bail, completed remains false. | bail_prevents_graduation |
UCAN — 5 properties
Models UCAN delegation chains with capability attenuation, signature verification, audience continuity, and audience binding.
| Tier | Property | Lean theorem |
|---|---|---|
| T1 | Delegation Transitivity Capability subset is transitive. | capSubset_trans |
| T1 | Capability Attenuation Leaf token's capability is always a subset of the root token's. | capability_attenuation |
| T2 | Signed Capability Attenuation Authenticated chain with verified signatures and audience continuity. | signed_capability_attenuation |
| T1 | Audience Binding A chain validated for audience A cannot be reused for audience B. | audience_binding |
| T2 | Audience-Attenuation Composition Audience and capability checks are independent gates. | audience_attenuation_composition |
Webhook — 4 properties
Models HMAC-SHA256 authentication for webhook push delivery and the message delivery lifecycle.
| Tier | Property | Lean theorem |
|---|---|---|
| T2 | Webhook HMAC Binding Attacker without the shared secret cannot verify payloads. | webhook_hmac_binding |
| T2 | Webhook Payload Integrity Different payloads produce different HMAC signatures. | webhook_payload_integrity |
| T1 | Delivery Fallback Failed webhook delivery preserves the message for poll retrieval. | delivery_fallback |
| T1 | Delivery Cleanup Successful delivery removes the message, preventing double-delivery. | delivery_cleanup |
Concrete Inhabitant Gates
Every abstract scheme has a compiling concrete instance that satisfies all axioms, proving the axiom set is consistent.
| Scheme | Inhabitant | Encoding |
|---|---|---|
| AEADScheme | concreteAEADScheme | encrypt k n p = myPair k (myPair n p) + 1 |
| HMACScheme | concreteHMACScheme | sign s p = myPair s p |
These are not realistic cryptographic implementations. They exist solely to prove axiom consistency via a binary Cantor pairing with a proven roundtrip.
Proof source: proofs/Layr0/*.lean · Toolchain: lean-toolchain pinned at · No Mathlib dependency.