ENC Protocol

Overview

ENC is a protocol for building append-only, cryptographically verifiable data structures. Every enclave is a sequenced event log with RBAC, Merkle proofs, and a single sequencer that orders and finalizes commits.

Architecture

Trust Model

Two query paths exist with fundamentally different trust properties:

DataView receives data via three methods, each requiring a role assignment:

Sequencer Model

Each enclave has a single sequencer — the node that orders and finalizes commits. The node that accepts the Manifest event becomes the sequencer, and its identity key is recorded in the Manifest's sequencer field. Multi-sequencer consensus is out of scope for v1.

The sequencer accepts valid commits, assigns seq and timestamp, signs events with seq_sig, maintains the SMT and CT trees, and delivers P/N to registered recipients.

Cryptographic Primitives

Five cryptographic axioms underpin every theorem. Each is instantiated with a concrete algorithm and modeled as idealized for formal reasoning.

The Canonical Hash Function

Every hash in ENC routes through H() — SHA-256 over deterministic CBOR encoding (RFC 8949 §4.2). CBOR is used only for hash computation, not transport. The v1 wire format is JSON.

-- H(fields...) = sha256(cborEncode(fields))
noncomputable def H (fields : List CborField) : Hash :=
  sha256 (cborEncode fields)

theorem H_injective :
    ∀ (a b : List CborField), H a = H b → a = b := by
  intro a b hab
  have hcbor := sha256_injective _ _ hab
  exact cborEncode_injective _ _ hcbor

Hash Prefix Registry

All hash operations use a unique single-byte prefix to prevent cross-domain collisions. Signature contexts use string prefixes for domain separation.

Wire Format

Transport uses JSON. Binary values are hex-encoded: hashes and public keys as 64-char hex (no prefix), signatures as 128-char hex, bitmasks as 0x-prefixed hex. CBOR encoding is used exclusively for hash pre-image computation.

Identity

An identity key is a 256-bit secp256k1 public key (id_pub). A client controls an identity by holding (or having authorized access to) the corresponding private key. The FTA formalizes four identity variants with cryptographic strength levels.

inductive Id where
  | anon                                   -- no key, strength 0
  | hold   (pub : PubKey)                  -- controls keypair, strength 1
  | share  (pub : PubKey) (k : Nat)        -- holds shard, strength 0
  | attest (pub : PubKey) (sig : Signature) -- proved via sig, strength 2

def Id.strength : Id → Nat
  | .anon       => 0    -- cannot create sessions
  | .hold _     => 1    -- can sign commits
  | .share _ _  => 0    -- single shard grants no capability
  | .attest _ _ => 2    -- proved via signature

Session Tokens

Stateless query authentication. A 68-byte token (136 hex chars) derived from the identity key, verifiable in O(1) EC math — no signature verification needed. Maximum lifetime: 7200 seconds (2 hours). Clock skew tolerance: ±60 seconds.

-- Client creates:
expires    = now + duration               -- max 7200 seconds
message    = "enc:session:" || be32(expires)
sig        = schnorr(sha256(message), id_priv)
r, s       = sig[0:32], sig[32:64]
session_pub = s · G                       -- point on secp256k1
token      = r || session_pub || be32(expires)

-- Node verifies in O(1) EC math:
t        = sha256(session_pub || seq_pub || enclave)
expected = r + sha256(r || from || message) · from
check: session_pub == expected

Per-Node Signer Derivation

Each session derives a per-node, per-enclave signer key for ECDH. This provides per-enclave key isolation: a compromised signer in Enclave A cannot decrypt messages for Enclave B.

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

Event Lifecycle

A Commit is a client proposal. An Event is the sequencer-endorsed result. A Receipt is the node-signed acknowledgment. The dual-signature chain binds author intent to sequencer ordering.

Hash Chain Construction

content_hash = sha256(utf8_bytes(content))                     -- raw SHA-256, not H()
commit_hash  = H(0x10, enclave, from, type, content_hash, exp, tags)
sig          = schnorr(commit_hash, from_priv)

event_hash   = H(0x11, timestamp, seq, sequencer, sig)
seq_sig      = schnorr(event_hash, sequencer_priv)
event_id     = sha256(seq_sig)                                 -- commits to both

enclave_id   = H(0x12, from, "Manifest", content_hash, tags)

Commit Structure

Tags

Tags provide node-level processing instructions (not query indexes). Content is opaque to the node; tags are understood.

Event Finalization

The node adds id, timestamp, sequencer, seq, seq_sig to produce the final event. For all events except Migrate (forced takeover), the sequencer field must match the current sequencer.

Validation Pipeline

theorem terminated_rejects_all
    (commit : Commit) (t : Timestamp)
    (dup : Bool) (ctx : AuthContext) (s : Schema) :
    validateCommit commit t .terminated dup ctx s =
      .reject .enclaveTerminated

theorem duplicate_rejected  -- dedup gate
    ... (hNotExp) (hNotFar) :
    validateCommit commit t ls true ctx s
      = .reject .duplicateCommit

Replay Protection

The node maintains a set of accepted commit hashes per enclave. Duplicate hashes are rejected. Hashes may be garbage-collected after exp + 60000 ms. Rejected commits are not added to the dedup set. Expiration window limit: MAX_EXP_WINDOW = 3600000 (1 hour). Clock skew tolerance: ±60 seconds.

Predefined Event Types

Only Content Events can be Updated or Deleted. AC Events are irreversible state transitions. Update/Delete events cannot themselves be U/D'd.

Update & Delete

U and D are logical operations implemented as new events referencing prior events via the r tag. The log remains append-only; originals are never mutated. Event status is tracked in the SMT Event Status namespace.

RBAC

Role-Based Access Control consists of an immutable Schema (fixed at Manifest creation) and mutable State (tracked in the SMT as 256-bit bitmasks). Changing the schema requires creating a new enclave.

Operations

Reserved Roles

Schema Entry Structure

{
  "event": "Grant",          // event type or "*" wildcard
  "role": "Admin",           // role name
  "ops": ["C"],              // permitted operations
  "target_roles": ["Member"] // privilege escalation bounds
}

Privilege Escalation Prevention

theorem revokeSelf_rejects_owner (ctx) (schema) :
    validateRevokeSelf ctx schema "Owner" = false

theorem forceMove_protects_owner_from
    (ctx) (schema) (fromBm toBm actual)
    (h : fromBm.hasBit bitOwner = true) :
    validateForceMove ctx schema fromBm toBm actual = false

theorem transfer_requires_owner (ctx)
    (h : ctx.actorBitmask.isOwner = false) :
    validateTransferOwner ctx = false

AC Events

Grant and Grant_Push are idempotent. Revoke and Grant for roles already held/not held succeed as no-ops. AC_Bundle uses simulated sequential validation: each operation is authorized against state after all preceding ops. If any fails, the entire bundle is rejected.

P (Push) & N (Notify)

Push delivers full events with at-least-once semantics (exponential backoff: 1s → 2x → max 5min, 10 retries). Notify delivers metadata only with best-effort. Each delivery is independent; per-type sequence counters (type_seq, 1-indexed, never resets) enable gap detection.

Enclave Lifecycle

Terminate and Migrate are mutually exclusive terminal states. The first terminal event wins. Lifecycle is derived from the event log, not stored in SMT.

Enclave State (SMT)

A single Sparse Merkle Tree stores both RBAC state and event status. Two namespaces, 168-bit depth (21-byte keys), same collision safety as Ethereum addresses (~10⁻³⁰ at 1B entries).

Key Construction

-- RBAC namespace (0x00):
path = 0x00 || sha256(id_pub)[0:160 bits]     -- 21 bytes

-- Event Status namespace (0x01):
path = 0x01 || sha256(event_id)[0:160 bits]  -- 21 bytes

Leaf Values

Hash Construction

leaf_hash  = H(0x20, key, value)
node_hash  = H(0x21, left_child, right_child)
empty_hash = sha256("")    -- hardcoded constant

State Binding

The SMT root (state_hash) is bound to the event log via CT leaf hashes. With bundling, state_hash is recorded per bundle. Two query modes: verified (CT-proven, may be stale) and current (fresh, no proof).

Proof System

Two Merkle trees provide verifiable state and history. The CT root alone commits to the entire event log AND current state in a single 32-byte hash.

Bundle Structure

bundle = {
  events: [event_id_0, ..., event_id_N],    -- ordered by seq
  state_hash: SMT root after last event
}

events_root:
  N=1 → event_ids[0]                        -- no tree needed
  N>1 → binary Merkle tree, internal = H(0x01, L, R)
         right-pad with last event_id to power of 2

leaf_hash = H(0x00, events_root, state_hash)

-- CT tree: bundles are leaves, RFC 9162 §2.1
-- Right-pad with last bundle's leaf_hash to power of 2

Full Event Proof (3 Layers)

Signed Tree Head (STH)

message = "enc:sth:" || be64(t) || be64(ts) || r   -- 8+8+8+32 = 56 bytes
sig     = schnorr(sha256(message), seq_priv)

-- Wire format:
{ "t": 1706000000000, "ts": 1000, "r": "<hex64>", "sig": "<hex128>" }

SMT Proof Wire Format

{
  "k": "<hex42>",     // 21-byte SMT key
  "v": "<hex|null>",  // leaf value (null = non-membership)
  "b": "<hex42>",     // 168-bit bitmap (which siblings present)
  "s": ["<hex64>"]   // non-empty sibling hashes only
}
// Verify: compute leaf → walk 167..0 using bitmap → compare root

Bundle Configuration

Set in Manifest (immutable). Close when size events accumulated OR timeout ms passed (whichever first). Timeout uses event timestamps, not wall clock. Default: size=256, timeout=5000. Set size=1 for per-event state verification.

Migration

Migration transfers an enclave to a new node while preserving the full event log and enclave identity. Only Owner can issue Migrate. Two modes:

{
  "new_sequencer": "<new_seq_pub>",
  "prev_seq": 1234,
  "ct_root": "<ct_root_at_prev_seq>"
}

Forced takeover verification: (1) replay all events computing SMT state, (2) verify SMT root matches state_hash in final bundle, (3) verify Migrate sender has Owner bit, (4) recompute CT root — must match ct_root, (5) verify commit signature, (6) verify prev_seq matches last event's seq.

Migration barrier: Once accepted, Migrate is the final event. The node rejects all pending commits, closes the bundle immediately. The ct_root checkpoint proves both log and state.

Backup pattern: To enable forced takeover, ensure someone has the full log — either Owner stores locally, or assign a Backup role with {"event": "*", "role": "Backup", "ops": ["P"]}.

Secrecy & Encryption

Two layers: transport encryption (always on, ECDH + XChaCha20Poly1305) and content encryption (application-chosen middleware). The node is a blind relay for encrypted content.

Transport Encryption

Nonce: random 24 bytes, prepended to ciphertext. Wire format: nonce || ciphertext || tag (min 40 bytes).

Content Encryption (Middleware)

theorem dm_roundtrip
    (senderPriv recipientPriv : ByteVec 32)
    (senderPub recipientPub : PubKey)
    (hSender : senderPub = derivePubKey senderPriv)
    (hRecipient : recipientPub = derivePubKey recipientPriv)
    (plaintext : ByteArray) :
    decryptFromSender recipientPriv senderPub
      (encryptForRecipient senderPriv recipientPub plaintext)
    = some plaintext

Node API

All communication uses a single endpoint (POST /) with request type detection, plus proof retrieval endpoints. Content-type: application/json.

Endpoints

WebSocket Model

First valid Query creates a subscription (node assigns sub_id). Events stream as encrypted messages. One connection supports multiple identities, each with their own session.

Filter

{
  "id": "<hex64> | [...]",
  "seq": "<uint> | [...] | Range",
  "type": "<string> | [...]",
  "from": "<hex64> | [...]",
  "tags": { "r": "abc..." },   // tag filter
  "timestamp": { "start_at": N, "end_before": M },
  "limit": 100,                // max 1000
  "reverse": false
}

Webhook Delivery

Node aggregates events into a single queue per (identity, url) pair across all enclaves. One push_seq counter for gap detection. Pull fallback via POST / with type: "Pull".

{
  "push_seq": 130,
  "push":   { "enclaves": [{ "enclave": "...", "events": [...] }] },
  "notify": { "enclaves": [{ "enclave": "...", "seq": 150 }] }
}

Error Codes

Registry

The Registry is an enclave with a DataView server providing discovery. Three event types: Reg_Node, Reg_Enclave, Reg_Identity — all Content Events within the Registry enclave, updatable and deletable.

Registration Flow

Reg_Node: Signed by seq_pub. Contains endpoints (max 10) with priority, protocols, enc_v. Reg_Enclave: Contains the full finalized Manifest event. For post-Transfer_Owner updates, includes owner_proof (STH + CT proof + SMT proof of Owner bit). Reg_Identity: Maps id_pub → enclaves (max 256 entries).

New submissions supersede existing entries for the same key (implicit Update in SMT). First Reg_Enclave for an enclave_id wins; conflicts are errors, not updates.