Aura Messaging Protocol (AMP)

AMP is a secure asynchronous messaging protocol for Aura. It operates within relational contexts and channels. The protocol provides strong post-compromise security and bounded forward secrecy without head-of-line blocking.

1. Scope and Goals

AMP assumes shared state in joint semilattice journals is canonical. Secrets derive locally from shared state combined with authority keys. Ratchet operations remain deterministic and recoverable.

The protocol targets four properties. No head-of-line blocking occurs during message delivery. Strong post-compromise security restores confidentiality after key exposure. Bounded forward secrecy limits exposure within skip windows. Deterministic recovery enables key rederivation from journal state.

1.2 Optimistic Operations Within Contexts

Key insight: Channels are encrypted substreams within an existing relational context. The relational context (established via invitation ceremony) already provides the shared secret foundation. This means:

No new key agreement - the relational context already provides the shared secret
Channel creation is local - just emit a ChannelCheckpoint fact into the existing context journal
Members must already share the context - you can't invite someone to a channel unless you already have a relational context with them

Channel creation and messaging are Category A (optimistic) operations because:

Both parties already derived the context root via the invitation ceremony
Channel facts sync via normal journal anti-entropy
Key derivation is deterministic: KDF(ContextRoot, ChannelId, epoch) → ChannelBaseKey

The encryption "just works" because the cryptographic foundation was established when the relationship was created. See Consensus - Operation Categories for the full classification.

1.1 Design Requirements

AMP addresses constraints that existing messaging protocols cannot satisfy.

Deterministic recovery requires all ratchet state to be derivable from replicated facts. The journal is the only durable state. Secrets derive from reduced journal state combined with authority keys. No device may maintain ratchet state that cannot be recovered by other devices in the authority.

Multi-device authorities require support for concurrent message sends from different devices within the same authority. External parties cannot observe which device sent a message. All devices must converge to the same ratchet position after merging facts.

Selective consistency requires both eventual consistency for message sends and strong agreement for epoch transitions. The protocol cannot assume a central ordering service.

Authorization integration requires every message send to pass through a guard chain before reaching the network. Authorization failure must prevent key derivation. Budget charges must be atomic with the send.

2. Channel Lifecycle Surface

The AmpChannelEffects trait defines the canonical API for AMP channel lifecycle and messaging. This trait lives in aura-core::effects::amp.

#![allow(unused)]
fn main() {
#[async_trait]
pub trait AmpChannelEffects: Send + Sync {
    async fn create_channel(&self, params: ChannelCreateParams) -> Result<ChannelId, AmpChannelError>;
    async fn close_channel(&self, params: ChannelCloseParams) -> Result<(), AmpChannelError>;
    async fn join_channel(&self, params: ChannelJoinParams) -> Result<(), AmpChannelError>;
    async fn leave_channel(&self, params: ChannelLeaveParams) -> Result<(), AmpChannelError>;
    async fn send_message(&self, params: ChannelSendParams) -> Result<AmpCiphertext, AmpChannelError>;
}
}

The create_channel method writes an AMP checkpoint and policy for a context-scoped channel. The close_channel method records a terminal epoch bump and policy closure. The join_channel and leave_channel methods record membership facts. The send_message method derives current channel state and returns AmpCiphertext containing the header and encrypted payload.

2.1 Implementations

The runtime implementation uses AmpChannelCoordinator in aura-protocol::amp::channel_lifecycle. The simulator implementation uses SimAmpChannels in aura-simulator::amp. The testkit provides MockEffects implementing AmpChannelEffects for deterministic unit tests.

2.2 TUI Wiring

The TUI routes EffectCommand variants through an optional AmpChannelEffects handle. Commands include CreateChannel, CloseChannel, and SendMessage. Events including ChannelCreated, ChannelClosed, and MessageReceived drive view updates.

Demo mode injects the simulator handler into SimulatedBridge. Alice and Carol agents use the same lifecycle as real clients while Bob remains human-controlled.

3. Terminology

3.1 Aura Terms

An authority is an account authority with a commitment tree and FROST keys. A relational context is shared state between authorities identified by ContextId. A journal is a CRDT OR-set of facts with monotone growth and deterministic reduction.

3.2 AMP Terms

A channel is a messaging substream scoped to a relational context. The channel epoch bounds post-compromise security and serves as the KDF base. The ratchet generation is a monotone position derived from reduced journal state. The skip window defines out-of-order tolerance with a default of 1024 generations.

A checkpoint is a journal fact anchoring ratchet windows. The alternating ratchet maintains two overlapping windows at boundaries. A pending bump is a proposed epoch transition awaiting consensus.

4. Commitment Tree Integration

The commitment tree defines authority structure and provides the foundation for key derivation. Each authority maintains an internal tree with branch nodes and leaf nodes. Leaf nodes represent devices holding threshold signing shares. Branch nodes represent subpolicies expressed as m-of-n thresholds.

#![allow(unused)]
fn main() {
pub struct TreeState {
    pub epoch: Epoch,
    pub root_commitment: TreeHash32,
    pub branches: BTreeMap<NodeIndex, BranchNode>,
    pub leaves: BTreeMap<LeafId, LeafNode>,
}
}

The TreeState represents the result of reducing all operations in the OpLog. The epoch field scopes all derived keys. The root_commitment field is a Merkle hash over the ordered tree structure. External parties see only the epoch and root commitment.

Tree operations modify device membership and policies. The AddLeaf operation inserts a new device. The RemoveLeaf operation removes an existing device. The ChangePolicy operation updates threshold requirements. The RotateEpoch operation increments the epoch and invalidates all derived keys.

Each operation appears in the journal as an attested operation signed by the required threshold of devices. The tree supports concurrent updates through deterministic conflict resolution.

graph TD
    A[Multiple Concurrent Ops] --> B[Group by Parent Commitment]
    B --> C[Select Winner by Hash Order]
    C --> D[Apply in Epoch Order]
    D --> E[Single TreeState]

The channel base key for a given ChannelId and epoch derives as KDF(TreeRoot, ChannelId, epoch). All devices in the authority compute the same base key.

5. Fact Structures

AMP uses facts inserted into the relational context journal. All facts are monotone. Reduction determines canonical state.

5.1 Channel Checkpoint

#![allow(unused)]
fn main() {
pub struct ChannelCheckpoint {
    pub context: ContextId,
    pub channel: ChannelId,
    pub chan_epoch: u64,
    pub base_gen: u64,
    pub window: u32,
    pub ck_commitment: Hash32,
    pub skip_window_override: Option<u32>,
}
}

Reduction chooses one canonical checkpoint per context, channel, and epoch tuple. The valid ratchet generation set is the union of two windows. Window A spans from base_gen to base_gen + window. Window B spans from base_gen + window + 1 to base_gen + 2 * window. Checkpoints enable deterministic recovery and serve as garbage collection anchors.

5.2 Proposed and Committed Epoch Bumps

#![allow(unused)]
fn main() {
pub struct ProposedChannelEpochBump {
    pub context: ContextId,
    pub channel: ChannelId,
    pub parent_epoch: u64,
    pub new_epoch: u64,
    pub bump_id: Hash32,
    pub reason: ChannelBumpReason,
}

pub struct CommittedChannelEpochBump {
    pub context: ContextId,
    pub channel: ChannelId,
    pub parent_epoch: u64,
    pub new_epoch: u64,
    pub chosen_bump_id: Hash32,
    pub consensus_id: Hash32,
}
}

Proposed bumps represent optimistic ratchet phase transitions. Committed bumps are finalized by Aura Consensus with 2f+1 witnesses. The new epoch always equals parent epoch plus one. Only one committed bump exists per parent epoch.

5.3 Channel Bump Reason

#![allow(unused)]
fn main() {
pub enum ChannelBumpReason {
    Routine,
    SuspiciousActivity,
    ConfirmedCompromise,
}
}

The Routine variant indicates cadence-based maintenance. The SuspiciousActivity variant indicates detected anomalies such as AEAD failures or ratchet conflicts. The ConfirmedCompromise variant requires immediate post-compromise security restoration. Both suspicious activity and confirmed compromise bypass routine spacing rules.

6. Derived Channel State

Reduction yields a ChannelEpochState struct containing the canonical epoch and derived state.

#![allow(unused)]
fn main() {
pub struct ChannelEpochState {
    pub chan_epoch: u64,
    pub pending_bump: Option<PendingBump>,
    pub last_checkpoint_gen: u64,
    pub current_gen: u64,
    pub skip_window: u32,
}

pub struct PendingBump {
    pub parent_epoch: u64,
    pub new_epoch: u64,
    pub bump_id: Hash32,
    pub reason: ChannelBumpReason,
}
}

The chan_epoch field holds the current canonical epoch. The pending_bump field holds an in-progress transition if one exists. The last_checkpoint_gen and current_gen fields track ratchet positions. The skip_window field determines out-of-order tolerance.

6.1 Skip Window Computation

The skip window derives from three sources in priority order. The checkpoint skip_window_override takes precedence. The channel policy fact applies if no override exists. The default of 1024 applies otherwise.

6.2 Critical Invariants

Before sending, a device must merge latest facts, reduce channel state, and use updated epoch and generation values. No device may send under stale epochs. Only one bump from epoch e to e+1 may be pending at a time. The new epoch always equals parent epoch plus one.

6.3 Ratchet Generation Semantics

The ratchet_gen value is not a local counter. It derives from reduced journal state. All devices converge to the same ratchet position after merging facts. Generation advances only when send or receive events occur consistent with checkpoint and dual-window rules. This guarantees deterministic recovery and prevents drift across devices.

7. Three-Level Key Architecture

AMP separates key evolution across three levels. Authority epochs provide identity-level post-compromise security. Channel epochs provide channel-level post-compromise security. Ratchet generations provide bounded forward secrecy within each epoch.

7.1 Authority Epochs

Authority epochs rotate the threshold key shares via DKG ceremony. Rotation invalidates all derived context keys. This is the strongest form of post-compromise security.

Authority epoch rotation occurs approximately daily or upon confirmed compromise. The rotation is independent of messaging activity. All relational contexts must re-derive their shared secrets after rotation.

7.2 Channel Epochs

Channel epochs provide post-compromise security at the channel level. Each epoch uses an independent base key derived from the tree root. Epoch rotation invalidates all keys from the previous epoch. The rotation is atomic. All devices observe the same epoch after merging journal facts.

The epoch bump lifecycle has two states. The stable state indicates that epoch e is finalized. The pending state indicates that an optimistic bump has been proposed. No new bump can be proposed while a bump is pending. This single-pending-bump invariant ensures linear epoch progression.

7.3 Ratchet Generations

Ratchet generations provide forward secrecy within each epoch. Message keys derive from the channel base key, generation, and direction.

#![allow(unused)]
fn main() {
pub struct AmpHeader {
    pub context: ContextId,
    pub channel: ChannelId,
    pub chan_epoch: u64,
    pub ratchet_gen: u64,
}
}

The AmpHeader contains the routing and ratchet information. The chan_epoch field identifies which base key to use. The ratchet_gen field identifies which generation key to derive. This header becomes the AEAD additional data.

Ratchet generation is not a local counter. It derives from reduced journal state. Devices compute the current generation by examining send and receive events in the reduced context state. All devices converge to the same ratchet position after merging facts.

8. Channel Epoch Bump Lifecycle

8.1 States

A channel has two states. The stable state indicates the epoch is finalized. The pending state indicates an optimistic bump awaits commitment.

8.2 Spacing Rule for Routine Bumps

AMP enforces a spacing rule for routine bumps. Let base_gen be the anchor generation from the canonical checkpoint. Let current_gen be the current ratchet generation. Let W be the skip window.

A routine bump from epoch e to e+1 requires current_gen - base_gen >= W / 2. With default W of 1024, this threshold equals 512 generations. This spacing ensures structural transitions do not occur too frequently.

Emergency bumps bypass this rule. Examples include multiple AEAD failures, conflicting ratchet commitments, unexpected epoch values, and explicit compromise signals.

8.3 State Transitions

In the stable state, if the spacing rule is satisfied and no bump is pending, the device inserts a ProposedChannelEpochBump and starts consensus. The device enters the pending state and uses the new epoch with alternating windows.

In the pending state, upon observing a committed bump, the device sets the new epoch and clears the pending bump. It may emit a new checkpoint and returns to the stable state.

8.4 Complete Lifecycle Sequence

The following diagram shows the complete double ratchet and epoch bump lifecycle between two devices.

sequenceDiagram
    participant A as Device A
    participant J as Journal
    participant C as Consensus
    participant B as Device B

    Note over A,B: Channel Creation (Epoch 0)
    A->>J: ChannelCheckpoint(epoch=0, base_gen=0, W=1024)
    J-->>B: Sync checkpoint fact
    B->>B: Reduce state → Epoch 0, gen=0

    Note over A,B: Normal Messaging (Ratchet Advancement)
    loop Messages within Window A [0..1024]
        A->>A: Merge facts, reduce state
        A->>A: Derive key(epoch=0, gen=N)
        A->>B: AmpHeader(epoch=0, gen=N) + ciphertext
        B->>B: Validate gen in [0..2048]
        B->>B: Derive key, decrypt
        B->>B: Advance receive ratchet
    end

    Note over A,B: Spacing Rule Satisfied (gen >= 512)
    A->>A: Check: current_gen - base_gen >= W/2
    A->>J: ProposedChannelEpochBump(0→1, reason=Routine)
    A->>C: Start consensus for bump

    Note over A,B: Pending State (Dual Windows Active)
    rect rgb(240, 240, 255)
        Note over A,B: Both epochs valid during transition
        A->>B: Messages use epoch=1 (optimistic)
        B->>B: Accept epoch=0 OR epoch=1
    end

    C->>C: Collect 2f+1 witness signatures
    C->>J: CommittedChannelEpochBump(0→1)
    J-->>A: Sync committed bump
    J-->>B: Sync committed bump

    Note over A,B: Epoch 1 Finalized
    A->>A: Clear pending_bump, set epoch=1
    B->>B: Clear pending_bump, set epoch=1
    A->>J: ChannelCheckpoint(epoch=1, base_gen=1024)

    Note over A,B: Continue in New Epoch
    loop Messages in Epoch 1
        A->>A: Derive key(epoch=1, gen=M)
        A->>B: AmpHeader(epoch=1, gen=M) + ciphertext
    end

    Note over A,B: Emergency Bump (Compromise Detected)
    B->>B: Detect AEAD failures > threshold
    B->>J: ProposedChannelEpochBump(1→2, reason=SuspiciousActivity)
    Note right of B: Bypasses spacing rule
    B->>C: Immediate consensus request
    C->>J: CommittedChannelEpochBump(1→2)

    Note over A,B: Post-Compromise Security Restored
    A->>A: Derive new base key for epoch=2
    B->>B: Derive new base key for epoch=2

This diagram illustrates four phases of the protocol. Channel creation establishes the initial checkpoint at epoch 0. Normal messaging advances the ratchet generation within dual windows. Routine bumps occur when spacing rules are satisfied and follow the consensus path. Emergency bumps bypass spacing for immediate post-compromise security.

9. Ratchet Windows

AMP uses an always-dual window model. Every checkpoint defines two consecutive skip windows providing a continuous valid range of 2W generations.

9.1 Window Layout

Given base generation G and skip window W, two windows are defined. Window A spans G to G+W. Window B spans G+W+1 to G+2W. The valid generation set is the union of both windows.

#![allow(unused)]
fn main() {
// Window layout for checkpoint at generation G with window W
let window_a = G..(G + W);
let window_b = (G + W + 1)..(G + 2*W);
let valid_gen_set = window_a.union(window_b);
}

flowchart LR
    subgraph "Valid Generation Range"
        A["Window A<br/>G to G+W"]
        B["Window B<br/>G+W+1 to G+2W"]
    end
    A --> B

This design eliminates boundary issues. No mode switches are required. The implementation remains simple with robust asynchronous tolerance.

9.2 Window Shifting

When a new checkpoint is issued, the new base generation is chosen far enough ahead per the spacing rule. The dual-window layout guarantees overlap with prior windows. Garbage collection can safely prune older checkpoints when they no longer affect valid generation ranges.

9.3 Asynchronous Delivery

The dual window design solves the asynchronous delivery problem. Messages may arrive out of order by up to W generations. During epoch transitions, messages may be sent under either the old or new epoch. The overlapping windows ensure that all valid messages can be decrypted.

Message derivation uses a KDF chain similar to Signal's construction but with key differences. AMP derives all ratchet state deterministically from replicated journal facts rather than device-local databases. This enables complete recovery across multiple devices without coordination.

10. Sending Messages

10.1 Message Header

#![allow(unused)]
fn main() {
pub struct AmpHeader {
    pub context: ContextId,
    pub channel: ChannelId,
    pub chan_epoch: u64,
    pub ratchet_gen: u64,
}
}

The header contains the context identifier, channel identifier, current epoch, and current generation. These fields form the additional authenticated data for AEAD encryption.

10.2 Reduce-Before-Send Rule

Before sending a message, a device must merge the latest journal facts. It must reduce the channel state to get the current epoch and generation. It must verify that the generation is within the valid window. Only then can it derive the message key and encrypt.

10.3 Send Procedure

Before sending, a device merges new facts and reduces channel state. It asserts that the current generation is within the valid generation set. It asserts the channel epoch is current.

If the spacing rule is satisfied and no bump is pending, the device proposes a new bump. The device derives the message key using a KDF with the channel base key, generation, and direction.

The device creates an AmpHeader, encrypts the payload with AEAD using the message key and header as additional data, and performs the guard chain. Guard evaluation runs over a prepared GuardSnapshot and emits EffectCommand items for async interpretation. The device then advances the local ratchet generation.

11. Receiving Messages

When receiving, a device merges new facts and reduces channel state. It checks that the message epoch is either the current or pending epoch. It checks that the generation is within the valid generation set.

The device rederives the message key using the same KDF parameters. It decrypts the payload using AEAD with the message key and header. It advances the local receive ratchet.

Messages outside valid windows or with unsupported epochs are rejected.

12. Guard Chain Integration

AMP integrates with Aura's guard chain for authorization and flow control. Every message send passes through CapabilityGuard, FlowBudgetGuard, JournalCouplingGuard, and LeakageTrackingGuard before reaching the transport.

Guard evaluation runs over a prepared GuardSnapshot and produces EffectCommand items. An async interpreter executes those commands only after the entire guard chain succeeds. Unauthorized or over-budget sends never touch the network.

#![allow(unused)]
fn main() {
let outcome = guard_chain.evaluate(&snapshot, &request);

if !outcome.is_authorized() {
    return Err(AuraError::authorization_failed("Guard denied"));
}

for cmd in outcome.effects {
    interpreter.execute(cmd).await?;
}
}

The snapshot captures the current capability frontier and flow budget state. Each guard emits EffectCommand items instead of performing I/O. The interpreter executes the resulting commands in production or simulation. Any failure returns locally without observable effects.

12.1 Flow Budgets

Flow budgets are replicated as spent counters in the journal. The spent counter for a context and peer pair is a monotone fact. The limit computes at runtime from Biscuit capabilities and sovereign policy. Before sending, the flow budget guard checks that spent + cost <= limit.

12.2 Receipts

Receipts provide accountability for multi-hop forwarding. Each relay hop produces a receipt containing the context, source, destination, epoch, cost, and signature. The receipt proves that the relay charged its budget before forwarding.

13. Recovery and Garbage Collection

13.1 Recovery

To recover, a device loads the relational context journal. It reduces to the latest committed epoch, checkpoint, and skip window. It rederives the channel base key from context root key, channel identifier, and epoch. It rederives ratchet state from the checkpoint and window generations.

graph TD
    A[Load Journal Facts] --> B[Reduce to TreeState]
    B --> C[Reduce to ChannelEpoch]
    C --> D[Compute Checkpoint]
    D --> E[Derive Base Key]
    E --> F[Ready to Message]

The recovery process requires no coordination. The device does not need to contact other participants. It does not need to request missing state. It only needs access to the journal facts. Once reduction completes, the device has the same view as all other participants.

13.2 Garbage Collection

AMP garbage collection maintains protocol safety while reclaiming storage. GC operates on checkpoints, proposed bumps, and committed bumps.

A checkpoint at generation G with window W can be pruned when a newer checkpoint exists at G' where G' exceeds G+2W. The newer checkpoint coverage must not overlap with the old checkpoint coverage. All messages within the old window must be processed or beyond the recovery horizon.

A proposed bump can be pruned when a committed bump supersedes it or when the epoch becomes stale. Committed bumps are retained as consensus evidence until full snapshot compaction.

13.3 Pruning Boundary

The safe pruning boundary for checkpoints is computed as the maximum checkpoint generation minus 2W minus a safety margin. The recommended safety margin is W/2 or 512 generations with default settings.

GC triggers when journal size exceeds threshold, checkpoint count exceeds maximum, manual compaction is requested, or snapshot creation initiates. See Maintenance for integration with the Aura snapshot system.

14. Security Properties

14.1 Forward Secrecy

Forward secrecy is bounded by the skip window size of 1024 within each epoch. Within a single epoch, an attacker who compromises a device learns at most W future message keys. Older epochs use independent base keys. Compromise of epoch e reveals nothing about epoch e-1.

14.2 Post-Compromise Security

Post-compromise security operates at two levels. Channel epoch bumps heal compromise of channel secret state. Context epoch bumps provide stronger PCS by healing compromise of context state. Channel bumps are frequent and cheap. Context bumps are rare and expensive.

The dual window mechanism provides continuous post-compromise healing. When an emergency bump occurs, the new epoch uses a fresh base key. Messages sent under the new epoch cannot be decrypted with the old base key. The overlapping windows ensure that honest messages in flight are not lost.

14.3 No Head-of-Line Blocking

The protocol accepts out-of-order messages up to W generations. Dual windows absorb boundary drift.

14.4 No Ratchet Forks

Consensus finalizes each epoch step. The epoch chain is always linear and monotone.

14.5 Deterministic Recovery

Checkpoints anchor the ratchet. Facts represent all shared state. Keys are always rederived deterministically. This property enables true multi-device messaging. All devices in an authority see the same messages. All devices can send and receive without coordinating who is currently active. The authority appears as a single messaging entity to external parties.

Keyboard shortcuts

Aura