Middleware Protocol

Encryption middleware between the application layer and the transport layer.

This document specifies the two middleware schemes that provide end-to-end encryption: ECDH for 1-to-1 direct messages, and Lazy MLS for group conversations. Both are Layer 3 in the architecture — they compose between the core protocol (Layer 2) and the application instances (Layer 4).

---

0. Encryption Schemes

Each enclave declares its encryption scheme in the AppManifest:

Public apps:   Scheme = (Direct, Static, ∅, ∅)     -- plaintext, no middleware
DM:            Scheme = (Direct, Epoch, ∅, ∅)       -- 
0
 per conversation
Group chat:    Scheme = (Tree N, Epoch, ttl?, rot?) -- Lazy MLS

Public apps (Timeline, Registry) bypass middleware entirely. Encrypted apps route all content through the appropriate scheme before it reaches the transport layer.

---

I. ECDH — Direct Message Encryption

ECDH provides 1-to-1 encryption for direct messages. Each conversation between two parties derives a shared key from their secp256k1 keypairs.

Key Derivation

shared_point = ECDH(my_priv, their_pub)    -- secp256k1 scalar multiplication
shared_x     = shared_point[1..33]          -- x-coordinate only (32 bytes)
key          = HKDF-SHA256(shared_x, info="enc:dm", L=32)

Both parties compute the same key: - Sender: ECDH(sender_priv, receiver_pub) → shared X → HKDF - Receiver: ECDH(receiver_priv, sender_pub) → same shared X → HKDF

Encrypt / Decrypt

encrypt(sender_priv, receiver_pub, plaintext):
  key       = deriveSharedKey(sender_priv, receiver_pub)
  nonce     = randomBytes(24)                           -- XChaCha20 nonce
  ct        = XChaCha20Poly1305.encrypt(key, nonce, plaintext)
  return    hex(nonce || ct)

decrypt(receiver_priv, sender_pub, wire):
  key       = deriveSharedKey(receiver_priv, sender_pub)
  nonce     = wire[0..24]
  ct        = wire[24..]
  return    XChaCha20Poly1305.decrypt(key, nonce, ct)

Transport Encryption (Client ↔︎ Node)

Separate from content encryption. All queries and responses are ECDH-encrypted with per-session derived signer keys:

Context          Client Key     Node Key    HKDF Label
─────────────    ───────────    ─────────   ──────────────
Query request    signer_priv    seq_pub     "enc:query"
Query response   signer_priv    seq_pub     "enc:response"
Push delivery    recipient      seq_priv    "enc:push"

Signer derivation:

t           = sha256(session_pub || seq_pub || enclave)
signer_priv = session_priv + t (mod n)
signer_pub  = session_pub + t·G

This ensures each session-enclave pair has unique transport keys, without exposing the long-term session key.

Lean Specification

namespace Enc.Middleware.ECDH
axiom deriveSharedKey : Type
axiom encryptDM : Type
axiom decryptDM : Type
end Enc.Middleware.ECDH

Generated output: apps/dm/sdk/lib/middleware.js (74 lines)

---

II. Lazy MLS — Group Encryption

MLS (Messaging Layer Security) provides forward-secret group encryption for chat. ENC uses a lazy variant: members don’t maintain a full ratchet tree. Instead, epoch secrets are distributed via the enclave, and sender ratchets provide per-message forward secrecy within each epoch.

Epoch Model

Epoch 0  →  Epoch 1  →  Epoch 2  →  ...
  │           │           │
  secret₀     secret₁     secret₂
  │           │           │
  ├─ sender ratchet A    ├─ sender ratchet A
  ├─ sender ratchet B    ├─ sender ratchet B
  └─ sender ratchet C    └─ sender ratchet C

Each epoch has: - An epoch secret (32 bytes), distributed encrypted to each member - A member set (public keys) - Per-sender ratchets for forward secrecy within the epoch

Epoch Transitions

addMember(pub):
  epoch      += 1
  members    += pub
  secret     = randomBytes(32)
  distribute secret encrypted to each member via ECDH

removeMember(pub):
  epoch      += 1
  members    -= pub
  secret     = randomBytes(32)
  distribute secret encrypted to remaining members

rotate():
  epoch      += 1
  secret     = randomBytes(32)
  distribute secret encrypted to all current members

Each transition increments the epoch and generates a fresh secret. Removed members cannot decrypt messages in the new epoch because they never receive the new epoch secret.

Sender Ratchets

Within an epoch, each sender maintains an independent ratchet:

sender_key(epoch, sender, generation):
  base      = HKDF(epoch_secret, info=sender_pub, L=32)
  key       = HKDF(base, info=generation.toString(), L=32)
  return    key

Each message increments the sender’s generation counter. This provides forward secrecy within an epoch — compromising a key at generation N does not reveal messages at generation N-1.

Encrypt / Decrypt

encrypt(epoch, plaintext):
  gen       = mySenderSeq[epoch]++
  key       = sender_key(epoch, myPub, gen)
  nonce     = randomBytes(24)
  ct        = XChaCha20Poly1305.encrypt(key, nonce, plaintext)
  header    = { epoch, generation: gen }
  return    header || nonce || ct

decrypt(epoch, sender_pub, wire):
  gen       = header.generation
  key       = sender_key(epoch, sender_pub, gen)
  nonce     = wire[header_len..header_len+24]
  ct        = wire[header_len+24..]
  return    XChaCha20Poly1305.decrypt(key, nonce, ct)

Welcome Messages

When a new member joins, they receive a welcome containing all epoch secrets they need to decrypt history (if the enclave allows history access):

welcome(new_member_pub, epoch_secrets[]):
  for each (epoch, secret) in epoch_secrets:
    encrypted = ECDH_encrypt(my_priv, new_member_pub, secret)
    emit Welcome event with encrypted payload

Frontend State

The frontend maintains MLS state across reconnections:

MLS State
  epoch           : number
  epochSecrets    : Map<epoch, Uint8Array>
  members         : Set<pubkey>
  senderRatchets  : Map<epoch, Map<sender, { key, generation }>>
  mySenderSeq     : Map<epoch, number>

This state is held in memory and rebuilt from the event log on reconnection. No MLS state is persisted to disk.

Lean Specification

namespace Enc.Middleware.MLS
axiom MLSMiddleware : Type
end Enc.Middleware.MLS

Generated output: apps/chat/sdk/lib/mls.js (397 lines)

---

III. Middleware Composition

The middleware layer composes cleanly between protocol and app:

App Layer (Timeline, DM, Chat)
    │
    │  encrypted = true?
    │
    ├── No  → plaintext commit → transport
    │
    └── Yes → middleware.encrypt(plaintext)
              │
              ├── DM    → ECDH.encrypt(signer, recipient, payload)
              └── Chat  → MLS.encrypt(epoch, payload)
                          │
                          transport (already double-encrypted)

On read, the reverse:

transport → raw event
    │
    ├── plaintext app → parse directly
    │
    └── encrypted app → middleware.decrypt(event)
                        │
                        ├── DM    → ECDH.decrypt(my_priv, sender_pub, ct)
                        └── Chat  → MLS.decrypt(epoch, sender_pub, ct)
                                    │
                                    parsed event

The application layer never sees ciphertext. The transport layer never sees plaintext. The middleware is the only bridge.

---

IV. Security Properties

Properties that should hold (and can be stated as Lean theorems):

-- 
0
 roundtrip
theorem ecdh_roundtrip :
  ∀ (a_priv b_pub : Key) (msg : Bytes),
    decrypt(b_priv, a_pub, encrypt(a_priv, b_pub, msg)) = msg

-- MLS forward secrecy
theorem mls_forward_secrecy :
  ∀ (epoch : Nat) (gen : Nat) (key : Key),
    sender_key(epoch, sender, gen) ≠ sender_key(epoch, sender, gen + 1)

-- 
0
 isolation
theorem epoch_isolation :
  ∀ (e1 e2 : Nat), e1 ≠ e2 →
    epochSecret(e1) ≠ epochSecret(e2)

-- Removed member cannot decrypt
theorem removed_member_excluded :
  ∀ (pub : Key) (epoch : Nat),
    pub ∉ members(epoch) →
    ¬ canDecrypt(pub, epoch)

---

V. Generated Output

Source	Generator	Output	Lines
Middleware/ECDH.lean	gen_js.py	apps/dm/sdk/lib/middleware.js	74
Middleware/MLS.lean	gen_js.py	apps/chat/sdk/lib/mls.js	397
(frontend)	—	apps/*/frontend/src/mls-state.js	~200
Total			~671