BACAP positions: a capability bound to one box on its stream

A cap paired with an index from another stream addresses a box nobody writes to. A position carries a proof Reaches cap.messageBoxIndex index that rules this out.

def Cryptlib.Protocols.BACAP.Types.instDecidableEqMessageBoxIndex.decEq (x✝ x✝¹ : MessageBoxIndex) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cryptlib.Protocols.BACAP.Types.instDecidableEqMessageBoxIndex : DecidableEq MessageBoxIndex

Equations

• Cryptlib.Protocols.BACAP.Types.instDecidableEqMessageBoxIndex = Cryptlib.Protocols.BACAP.Types.instDecidableEqMessageBoxIndex.decEq

The ratchet as an iterate

def Cryptlib.Protocols.BACAP.Types.ratchet (m : MessageBoxIndex) : MessageBoxIndex

One ratchet step under BLAKE2b-512.

Equations

• Cryptlib.Protocols.BACAP.Types.ratchet m = Cryptlib.Protocols.BACAP.Ratchet.advanceOne m Cryptlib.Primitives.Hash.HKDF.blake2b512_hkdf

theorem Cryptlib.Protocols.BACAP.Types.ratchet_idx64_toNat (m : MessageBoxIndex) (h : m.idx64.toNat + 1 < 2 ^ 64) : (ratchet m).idx64.toNat = m.idx64.toNat + 1

theorem Cryptlib.Protocols.BACAP.Types.iterate_idx64_toNat (k : ℕ) (m : MessageBoxIndex) : m.idx64.toNat + k < 2 ^ 64 → (ratchet^[k] m).idx64.toNat = m.idx64.toNat + k

theorem Cryptlib.Protocols.BACAP.Types.advanceIndexTo_eq (m : MessageBoxIndex) (target : UInt64) : m.advanceIndexTo target = if target < m.idx64 then none else some (ratchet^[target.toNat - m.idx64.toNat] m)

advanceIndexTo is the ratchet iterated up to the target, or none going backwards.

Streams

def Cryptlib.Protocols.BACAP.Types.Reaches (start idx : MessageBoxIndex) : Prop

idx is k ratchet steps on from start, for some k that does not overflow idx64.

Equations

• Cryptlib.Protocols.BACAP.Types.Reaches start idx = ∃ (k : ℕ), start.idx64.toNat + k < 2 ^ 64 ∧ Cryptlib.Protocols.BACAP.Types.ratchet^[k] start = idx

theorem Cryptlib.Protocols.BACAP.Types.Reaches.refl (m : MessageBoxIndex) : Reaches m m

theorem Cryptlib.Protocols.BACAP.Types.Reaches.idx64 {start idx : MessageBoxIndex} (h : Reaches start idx) : ∃ (k : ℕ), idx.idx64.toNat = start.idx64.toNat + k ∧ ratchet^[k] start = idx

theorem Cryptlib.Protocols.BACAP.Types.Reaches.iterate {start idx : MessageBoxIndex} (h : Reaches start idx) (j : ℕ) (hj : idx.idx64.toNat + j < 2 ^ 64) : Reaches start (ratchet^[j] idx)

def Cryptlib.Protocols.BACAP.Types.maxContainsWalk : ℕ

The furthest contains walks the ratchet.

Equations

• Cryptlib.Protocols.BACAP.Types.maxContainsWalk = 2 ^ 18

inductive Cryptlib.Protocols.BACAP.Types.BACAPError : Type

Why a BACAP operation refused its input. openFailed covers both a bad signature and an AEAD failure.

• indexNotInChannel : BACAPError
• indexTooFar : BACAPError
• emptyBox : BACAPError
• boxMismatch : BACAPError
• openFailed : BACAPError

@[instance_reducible]

instance Cryptlib.Protocols.BACAP.Types.instDecidableEqBACAPError : DecidableEq BACAPError

Equations

• Cryptlib.Protocols.BACAP.Types.instDecidableEqBACAPError x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cryptlib.Protocols.BACAP.Types.instReprBACAPError : Repr BACAPError

Equations

• Cryptlib.Protocols.BACAP.Types.instReprBACAPError = { reprPrec := Cryptlib.Protocols.BACAP.Types.instReprBACAPError.repr }

def Cryptlib.Protocols.BACAP.Types.instReprBACAPError.repr : BACAPError → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.BACAP.Types.checkReaches (start idx : MessageBoxIndex) : Except BACAPError (PLift (Reaches start idx))

idx with a proof it is on the stream from start, or why not.

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Protocols.BACAP.Types.checkReaches_ok_iff (start idx : MessageBoxIndex) : (∃ (p : PLift (Reaches start idx)), checkReaches start idx = Except.ok p) ↔ ∃ k ≤ maxContainsWalk, start.idx64.toNat + k < 2 ^ 64 ∧ ratchet^[k] start = idx

checkReaches accepts exactly the indices a bounded number of ratchet steps on.

Contains

def Cryptlib.Protocols.BACAP.Types.ReadCap.contains (rc : ReadCap) (idx : MessageBoxIndex) : Except BACAPError Unit

.ok () if the ratchet reaches idx from the cap's index within maxContainsWalk steps.

Equations

• rc.contains idx = Except.map (fun (x : PLift (Cryptlib.Protocols.BACAP.Types.Reaches rc.messageBoxIndex idx)) => ()) (Cryptlib.Protocols.BACAP.Types.checkReaches rc.messageBoxIndex idx)

def Cryptlib.Protocols.BACAP.Types.WriteCap.contains (wc : WriteCap) (idx : MessageBoxIndex) : Except BACAPError Unit

See ReadCap.contains.

Equations

• wc.contains idx = wc.readCap.contains idx

theorem Cryptlib.Protocols.BACAP.Types.contains_ok_iff (rc : ReadCap) (idx : MessageBoxIndex) : rc.contains idx = Except.ok () ↔ ∃ k ≤ maxContainsWalk, rc.messageBoxIndex.idx64.toNat + k < 2 ^ 64 ∧ ratchet^[k] rc.messageBoxIndex = idx

contains accepts idx iff idx is the cap's index ratcheted at most maxContainsWalk times.

theorem Cryptlib.Protocols.BACAP.Types.contains_ok_iff_advanceIndexTo (rc : ReadCap) (idx : MessageBoxIndex) : rc.contains idx = Except.ok () ↔ rc.messageBoxIndex.idx64 ≤ idx.idx64 ∧ idx.idx64.toNat - rc.messageBoxIndex.idx64.toNat ≤ maxContainsWalk ∧ rc.messageBoxIndex.advanceIndexTo idx.idx64 = some idx

contains_ok_iff, phrased with advanceIndexTo.

Opening a box

def Cryptlib.Protocols.BACAP.Types.zeroBox : Primitives.Sign.Ed25519Blinded.PubBytes

The all-zero box ID, which a reply carries when the box was empty.

Equations

• Cryptlib.Protocols.BACAP.Types.zeroBox = Vector.replicate 32 0

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.openForContext (m : MessageBoxIndex) (rc : ReadCap) (ctx : ByteArray) (box : Primitives.Sign.Ed25519Blinded.PubBytes) (ciphertext : ByteArray) (sig : Primitives.Sign.Ed25519Blinded.SigBytes) : Except BACAPError ByteArray

Check the box is the one rc and this index derive under ctx, then verify and decrypt. The check rejects a tombstone signed for another box.

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Protocols.BACAP.Types.openForContext_box {m : MessageBoxIndex} {rc : ReadCap} {ctx : ByteArray} {box : Primitives.Sign.Ed25519Blinded.PubBytes} {ct : ByteArray} {sig : Primitives.Sign.Ed25519Blinded.SigBytes} {pt : ByteArray} (h : m.openForContext rc ctx box ct sig = Except.ok pt) : box = m.boxIDForContext rc ctx

openForContext only succeeds for the box the cap and index derive.

theorem Cryptlib.Protocols.BACAP.Types.openForContext_encrypt (wc : WriteCap) (m : MessageBoxIndex) (ctx pt : ByteArray) (hz : (m.encryptForContext wc ctx pt).1 ≠ zeroBox) : m.openForContext wc.readCap ctx (m.encryptForContext wc ctx pt).1 (m.encryptForContext wc ctx pt).2.1 (m.encryptForContext wc ctx pt).2.2 = Except.ok pt

An encrypted box opens to its plaintext at its own index, unless its box ID is all zeros.

theorem Cryptlib.Protocols.BACAP.Types.openForContext_tombstone (wc : WriteCap) (m : MessageBoxIndex) (ctx : ByteArray) (hz : (m.signBox wc ctx ByteArray.empty).1 ≠ zeroBox) : m.openForContext wc.readCap ctx (m.signBox wc ctx ByteArray.empty).1 ByteArray.empty (m.signBox wc ctx ByteArray.empty).2 = Except.ok ByteArray.empty

A tombstone opens as empty at its own box, unless that box ID is all zeros.

Positions

structure Cryptlib.Protocols.BACAP.Types.ReadPosition : Type

A read cap and one box on its stream.

• cap : ReadCap
• index : MessageBoxIndex
• onStream : Reaches self.cap.messageBoxIndex self.index

structure Cryptlib.Protocols.BACAP.Types.WritePosition : Type

A write cap and one box on its stream.

• cap : WriteCap
• index : MessageBoxIndex
• onStream : Reaches self.cap.messageBoxIndex self.index

def Cryptlib.Protocols.BACAP.Types.ReadCap.start (rc : ReadCap) : ReadPosition

The position of the cap's own index.

Equations

• rc.start = { cap := rc, index := rc.messageBoxIndex, onStream := ⋯ }

def Cryptlib.Protocols.BACAP.Types.WriteCap.start (wc : WriteCap) : WritePosition

The position of the cap's own index.

Equations

• wc.start = { cap := wc, index := wc.messageBoxIndex, onStream := ⋯ }

def Cryptlib.Protocols.BACAP.Types.ReadCap.positionAt (rc : ReadCap) (idx : MessageBoxIndex) : Except BACAPError ReadPosition

The position of idx, after checking it is on this cap's stream.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.BACAP.Types.WriteCap.positionAt (wc : WriteCap) (idx : MessageBoxIndex) : Except BACAPError WritePosition

The position of idx, after checking it is on this cap's stream.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.BACAP.Types.ReadPosition.next (p : ReadPosition) : Option ReadPosition

The next box, or none at the end of the index space.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.BACAP.Types.ReadPosition.advanceTo (p : ReadPosition) (target : UInt64) : Option ReadPosition

The box at target, or none if that is behind this one.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.BACAP.Types.WritePosition.next (p : WritePosition) : Option WritePosition

The next box, or none at the end of the index space.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.BACAP.Types.WritePosition.advanceTo (p : WritePosition) (target : UInt64) : Option WritePosition

The box at target, or none if that is behind this one.

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Protocols.BACAP.Types.ReadPosition.next_index (p : ReadPosition) : Option.map (fun (x : ReadPosition) => x.index) p.next = p.index.nextIndex

next moves a position exactly as nextIndex moves its index.

theorem Cryptlib.Protocols.BACAP.Types.ReadPosition.advanceTo_index (p : ReadPosition) (target : UInt64) : Option.map (fun (x : ReadPosition) => x.index) (p.advanceTo target) = p.index.advanceIndexTo target

advanceTo moves a position exactly as advanceIndexTo moves its index.

theorem Cryptlib.Protocols.BACAP.Types.WritePosition.next_index (p : WritePosition) : Option.map (fun (x : WritePosition) => x.index) p.next = p.index.nextIndex

theorem Cryptlib.Protocols.BACAP.Types.WritePosition.advanceTo_index (p : WritePosition) (target : UInt64) : Option.map (fun (x : WritePosition) => x.index) (p.advanceTo target) = p.index.advanceIndexTo target

def Cryptlib.Protocols.BACAP.Types.WritePosition.readPosition (p : WritePosition) : ReadPosition

The read position of the same box.

Equations

• p.readPosition = { cap := p.cap.readCap, index := p.index, onStream := ⋯ }

def Cryptlib.Protocols.BACAP.Types.ReadPosition.boxID (p : ReadPosition) (ctx : ByteArray) : Primitives.Sign.Ed25519Blinded.PubBytes

Equations

• p.boxID ctx = p.index.boxIDForContext p.cap ctx

def Cryptlib.Protocols.BACAP.Types.WritePosition.boxID (p : WritePosition) (ctx : ByteArray) : Primitives.Sign.Ed25519Blinded.PubBytes

Equations

• p.boxID ctx = p.index.boxIDForContext p.cap.readCap ctx

def Cryptlib.Protocols.BACAP.Types.ReadPosition.open (p : ReadPosition) (ctx : ByteArray) (box : Primitives.Sign.Ed25519Blinded.PubBytes) (ciphertext : ByteArray) (sig : Primitives.Sign.Ed25519Blinded.SigBytes) : Except BACAPError ByteArray

Verify and decrypt the box at this position. See MessageBoxIndex.openForContext.

Equations

• p.open ctx box ciphertext sig = p.index.openForContext p.cap ctx box ciphertext sig

def Cryptlib.Protocols.BACAP.Types.WritePosition.encrypt (p : WritePosition) (ctx plaintext : ByteArray) : Primitives.Sign.Ed25519Blinded.PubBytes × ByteArray × Primitives.Sign.Ed25519Blinded.SigBytes

Returns (box ID, ciphertext, signature).

Equations

• p.encrypt ctx plaintext = p.index.encryptForContext p.cap ctx plaintext

def Cryptlib.Protocols.BACAP.Types.WritePosition.tombstone (p : WritePosition) (ctx : ByteArray) : Primitives.Sign.Ed25519Blinded.PubBytes × Primitives.Sign.Ed25519Blinded.SigBytes

Sign the empty payload for this box; returns (box ID, signature).

Equations

• p.tombstone ctx = p.index.signBox p.cap ctx ByteArray.empty

theorem Cryptlib.Protocols.BACAP.Types.WritePosition.open_tombstone (p : WritePosition) (ctx : ByteArray) (hz : (p.tombstone ctx).1 ≠ zeroBox) : p.readPosition.open ctx (p.tombstone ctx).1 ByteArray.empty (p.tombstone ctx).2 = Except.ok ByteArray.empty

A write position's tombstone opens as empty at its own read position.

theorem Cryptlib.Protocols.BACAP.Types.ReadPosition.reaches (p : ReadPosition) : Reaches p.cap.messageBoxIndex p.index

Every position addresses a box on its cap's stream.

theorem Cryptlib.Protocols.BACAP.Types.WritePosition.reaches (p : WritePosition) : Reaches p.cap.messageBoxIndex p.index

Serialization: the cap's bytes followed by the index's

def Cryptlib.Protocols.BACAP.Types.ReadPosition.toBytes (p : ReadPosition) : Vector UInt8 (ReadCapSize + MessageBoxIndexSize)

Equations

• p.toBytes = Cryptlib.Protocols.BACAP.Types.marshalReadCap p.cap ++ Cryptlib.Protocols.BACAP.Types.marshalMessageBoxIndex p.index

def Cryptlib.Protocols.BACAP.Types.WritePosition.toBytes (p : WritePosition) : Vector UInt8 (WriteCapSize + MessageBoxIndexSize)

Equations

• p.toBytes = Cryptlib.Protocols.BACAP.Types.marshalWriteCap p.cap ++ Cryptlib.Protocols.BACAP.Types.marshalMessageBoxIndex p.index

def Cryptlib.Protocols.BACAP.Types.ReadPosition.ofBytes (data : Vector UInt8 (ReadCapSize + MessageBoxIndexSize)) : Option ReadPosition

Decode a position, checking its index is on its cap's stream.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.BACAP.Types.WritePosition.ofBytes (data : Vector UInt8 (WriteCapSize + MessageBoxIndexSize)) : Option WritePosition

Decode a position, checking its index is on its cap's stream.

Equations

• One or more equations did not get rendered due to their size.