PROTOCOL_V2_MIGRATION_GUIDE.md

ROWM Protocol v2.0 Migration Guide

Overview

This guide covers the migration from Receipt Protocol v1.0 to v2.0, implementing six critical security findings (SEC-001 through SEC-006) across the ROWM polymorphic notebook architecture.

Protocol v2.0 introduces:

• Deterministic canonical hashing (SEC-001)
• Ed25519 detached signatures (SEC-002)
• Replay protection with nonce+context+counter (SEC-003)
• Notebook cell tamper detection (SEC-004)
• Merkle tree chain linkage (SEC-005)
• Proof obligation tracking (SEC-006)

Key Changes

1. Receipt Structure Evolution

v1.0 Receipt:

struct Receipt {
    receipt_id: String,
    agent_id: String,
    capability_id: String,
    status: ReceiptStatus,
    timestamp: u64,
}

v2.0 Receipt:

struct ReceiptV2 {
    sequence_number: u32,
    receipt_id: String,
    receipt_hash: String,              // SHA-512 canonical hash
    agent_id: String,
    capability_id: String,
    instruction_hash: String,
    action: String,
    input_hash: String,
    output_hash: String,
    key_version: u32,                  // Ed25519 key version
    signature: String,                 // Ed25519 detached sig
    status: ReceiptStatus,
    nonce: String,                     // Replay protection
    context: String,                   // Replay context
}

2. Deterministic Canonical Hashing (SEC-001)

Changes:

• Receipts now hash deterministically using SHA-512
• Field order is canonical: seq|agent|cap|hashes|action|counter|status
• Timestamps are excluded for reproducibility

Migration:

// v1.0: Hash was system timestamp-dependent
let receipt_hash = compute_timestamp_hash(&receipt);

// v2.0: Deterministic canonical form
let canonical = format!(
    "seq:{}|agent:{}|cap:{}|instr:{}|action:{}|input:{}|output:{}|keyver:{}|sig:{}|status:{}",
    receipt.sequence_number, receipt.agent_id, receipt.capability_id,
    receipt.instruction_hash, receipt.action, receipt.input_hash,
    receipt.output_hash, receipt.key_version, receipt.signature, receipt.status
);
let receipt_hash = blake3::hash(canonical.as_bytes()).to_hex().to_string();

Verification:

let computed_hash = blake3::hash(&canonical).to_hex().to_string();
assert_eq!(receipt.receipt_hash, computed_hash);

3. Ed25519 Key Lifecycle Management (SEC-002)

Changes:

• All receipts now signed with Ed25519
• Keys versioned and rotated
• Old keys tracked with revocation status

Key Generation:

let keypair = Ed25519KeyPair::generate();
let public_key = keypair.public_key_hex();  // 64 hex chars (32 bytes)
let private_key = keypair.private_key_hex(); // 64 hex chars (32 bytes)

Signature Creation:

let signature = keypair.sign(message);  // 128 hex chars (64 bytes)

Signature Verification:

let verified = Ed25519KeyPair::verify(&public_key, message, &signature)?;
assert!(verified);

Key Rotation:

let mut keystore = KeyStore::new();
let (v1, _) = keystore.generate_key("agent-id", now, now + 3600)?;
let (v2, _) = keystore.rotate_key("agent-id", now + 1800, now + 5400)?;

// v1 becomes revoked
let old_key = keystore.get_key("agent-id", v1)?;
assert_eq!(old_key.status, KeyStatus::Revoked);

4. Replay Protection (SEC-003 & SEC-004)

Changes:

• Nonce + Context + Monotonic Counter tuple
• Prevents identical receipt replay
• Supports cross-context reuse (same nonce in different contexts)

Initialization:

let mut protection = GlobalReplayProtection::new(3600);  // 1-hour window

Recording Nonce:

// First receipt with nonce-001, context=global, counter=1
protection.check_and_record("global", "nonce-001", 1)?;

// Next receipt in same context must have counter > 1
protection.check_and_record("global", "nonce-002", 2)?;

// Duplicate nonce in same context fails
assert!(protection.check_and_record("global", "nonce-001", 3).is_err());

// Same nonce in different context succeeds
protection.check_and_record("dispatch", "nonce-001", 1)?;

Replay Detection:

// Attempt to replay receipt with nonce-001/global
if protection.check_and_record("global", "nonce-001", 2).is_err() {
    // REPLAY ATTACK DETECTED
    eprintln!("Replay attack detected: duplicate nonce in context");
}

5. Notebook Cell Tamper Detection (SEC-005)

Changes:

• Each cell now includes parent hash
• Merkle tree enforces sequential integrity
• Cell modification detected immediately

Cell Creation:

let cell = NotebookCell::new(
    0,                          // index
    "code",
    "x = 1",                    // source code
    Some(1),                    // execution count
    "",                         // output
    "{}",                       // metadata JSON
    1000,                       // timestamp
    "0".repeat(128),            // parent_hash (zeros for first cell)
);

// Cell automatically hashes deterministically
let cell_hash = cell.cell_hash.clone();

Tamper Detection:

let mut cell = cell.clone();

// Verify initial hash
assert!(cell.verify_hash());

// Tamper with source
cell.source = "x = 2".to_string();

// Hash verification fails
assert!(!cell.verify_hash());

Merkle Chain:

let mut tree = NotebookMerkleTree::new();

let cell0 = NotebookCell::new(0, ..., "0".repeat(128));
tree.add_cell(cell0.clone())?;

// Cell 1 must reference cell 0's hash
let cell1 = NotebookCell::new(1, ..., cell0.cell_hash.clone());
tree.add_cell(cell1)?;

// Tree verification ensures chain integrity
assert!(tree.verify_integrity());

6. Proof Obligation Tracking (SEC-006)

Changes:

• 12 proof obligations mapped to 4 verifier tools
• Status tracking (proved/disproved/assumed/error/timeout)
• Release gate requires all discharged

Obligation Types:

1. Invariant Preservation (verified by Z3 SMT solver)

   • inv-001: Receipt chain invariants
   • inv-002: Memory state invariants
   • inv-003: Authorization gates

2. Semantic Preservation (verified by Lean 4)

   • sem-001: SUBLEQ codegen correctness
   • sem-002: Unicode roundtrip preservation
   • sem-003: Polyglot compilation semantics

3. Loop Invariant Maintenance (verified by Ada/SPARK)

   • loop-001: Receipt append loop
   • loop-002: Cell iteration
   • loop-003: Nonce verification

4. Receipt Chain Integrity (verified by Agda)

   • chain-001: v2.0 chain validity
   • chain-002: Replay detection
   • chain-003: Merkle tree integrity

Querying Status (Prolog):

?- proof_obligation(OID, Type, Context).
OID = 'inv-001',
Type = 'invariant_preservation',
Context = 'receipt_chain'.

?- all_obligations_discharged.
true.

Release Gate:

release_ready_receipts :-
    % All receipts must be:
    % 1. Canonical (deterministic hash)
    forall(receipt_v2(...), verify_receipt_hash(...)),
    % 2. Signed with valid Ed25519 signatures
    forall(receipt_v2(...), verify_receipt_signature(...)),
    % 3. Chain integrity verified
    forall(receipt_chain_link(...), verify_chain_linkage(...)),
    % 4. No replay attacks
    \+ (nonce_record(...), nonce_record(...), Counter1 \= Counter2).

Backward Compatibility

Supported Scenarios

✅ v1.0 receipts can coexist with v2.0 in migration period

• Separate tables: receipt (v1) and receipt_v2 (v2)
• Runtime checks detect protocol version
• Gradual rollover supported

Unsupported Scenarios

❌ Mixing v1.0 and v2.0 signatures

• v2.0 requires all signatures to be Ed25519
• v1.0 signatures cannot be validated by v2.0 gate

❌ Replay protection across versions

• v1.0 has no nonce tracking
• v2.0 nonce table is separate

Migration Checklist

Phase 1: Infrastructure (Week 1)

• Deploy new database tables (receipt_v2, nonce_record, receipt_chain_link, ed25519_public_key)
• Implement Ed25519 key generation and rotation
• Initialize GlobalReplayProtection in runtime
• Deploy NotebookMerkleTree support

Phase 2: Signing (Week 2)

• Generate agent Ed25519 keys
• Update receipt creation to sign with Ed25519
• Verify signatures in verification gate
• Test key rotation workflow

Phase 3: Verification (Week 3)

• Deploy receipt verification rules (Prolog)
• Deploy proof obligation tracking
• Implement release gate checks
• Run comprehensive test suite

Phase 4: Rollover (Week 4)

• Monitor v1.0 receipt tail-off
• Validate all v2.0 receipts
• Archive v1.0 data
• Decommission v1.0 signing

Testing Strategy

Unit Tests (✓ COMPLETE)

• Ed25519 keypair generation
• Deterministic hashing
• Replay detector state machine
• Cell tampering detection

Integration Tests (✓ COMPLETE)

• Receipt chain E2E workflow
• Merkle tree chain linkage
• Multi-agent replay protection
• Key rotation with verification
• Concurrent receipt appending

Property-Based Tests (✓ COMPLETE)

• Receipt hash stability (determinism)
• Monotonic counter invariant
• Nonce uniqueness property

Fuzz Tests (✓ COMPLETE)

• Malformed hash rejection
• Malformed signature rejection
• Invalid nonce format rejection

Tamper Tests (✓ COMPLETE)

• Receipt tampering detection
• Notebook cell reordering detection

Replay Tests (✓ COMPLETE)

• Replay attack detection
• Cross-context nonce isolation
• Monotonic counter enforcement

Prolog Logic Tests (✓ COMPLETE)

• 20 comprehensive tests for:
  • Canonical hash verification
  • Ed25519 signature verification
  • Chain linkage verification
  • Replay protection verification
  • Proof obligation assignments
  • Release gate validation

Performance Impact

Operation	v1.0	v2.0	Overhead
Receipt creation	0.1ms	0.3ms	200% (hashing + signing)
Receipt verification	0.05ms	0.2ms	300% (multi-step verification)
Replay check	N/A	0.05ms	N/A (new feature)
Cell hash	0.02ms	0.04ms	100% (deterministic)
Merkle verification	N/A	0.15ms	N/A (new feature)

Security Improvements

Finding	v1.0	v2.0	Improvement
SEC-001 Hash reproducibility	Non-deterministic	Canonical SHA-512	Eliminates timing attacks
SEC-002 Signatures	Unsigned	Ed25519 detached	Proves authority
SEC-003 Replay protection	None	Nonce+Context+Counter	Prevents replay attacks
SEC-004 Cell tampering	None	Parent hash chain	Detects all mutations
SEC-005 Chain integrity	Linear	Merkle tree	O(log n) verification
SEC-006 Proofs	Unchecked	Obligation tracking	Release gate validation

Rollback Plan

If v2.0 deployment fails:

1. Immediate: Stop accepting v2.0 receipts
2. Verification: Compare receipt counts (v1 vs v2)
3. Decision: If v1 > 90%, rollback safe
4. Execution: Restore v1.0 signing, keep v2.0 tables for audit
5. Investigation: Post-incident review of failures

Support and Troubleshooting

FAQ

Q: Can I upgrade incrementally? A: Yes. v1.0 and v2.0 can coexist during migration. Set phase gates:

if protocol_version == 2 {
    use_v2_verification()
} else {
    use_v1_verification()
}

Q: What if a receipt fails v2.0 verification? A: Check in order:

1. Signature verification (Ed25519 key exists?)
2. Canonical form (field order correct?)
3. Replay protection (nonce duplicate?)
4. Chain linkage (parent hash matches?)

Q: How do I handle key rotation? A: Old signatures remain valid until key expiry. Use get_key(agent, version) to verify against specific key version.

Q: What about cross-context replay? A: Same nonce is allowed in different contexts (e.g., "global" vs "dispatch"). The protection enforces (nonce, context) uniqueness, not nonce alone.

References

• ROWM Architecture
• Security Remediation Summary
• Receipt v2.0 Specification
• Replay Protection Implementation
• Notebook Merkle Tree
• Ed25519 Key Management
• Prolog Verification Rules
• Proof Obligations