BACAP ratchet and per-context key derivation

def Cryptlib.Protocols.BACAP.Ratchet.deriveKForContext (m : Types.MessageBoxIndex) (hkdf : Primitives.Hash.HKDF.HKDF) (ctx : ByteArray) : Vector UInt8 32

K_i^ctx = HKDF-Expand(HKDF-Extract(salt=ctx, IKM=K_i), info=empty, 32).

Equations

• Cryptlib.Protocols.BACAP.Ratchet.deriveKForContext m hkdf ctx = Vector.ofFn fun (i : Fin 32) => (hkdf.expand (hkdf.extract ctx { data := m.curBlindingFactor.toArray }) ByteArray.empty 32)[i]!

def Cryptlib.Protocols.BACAP.Ratchet.deriveEForContext (m : Types.MessageBoxIndex) (hkdf : Primitives.Hash.HKDF.HKDF) (ctx : ByteArray) : Vector UInt8 32

E_i^ctx = HKDF-Expand(HKDF-Extract(salt=ctx, IKM=E_i), info=empty, 32).

Equations

• Cryptlib.Protocols.BACAP.Ratchet.deriveEForContext m hkdf ctx = Vector.ofFn fun (i : Fin 32) => (hkdf.expand (hkdf.extract ctx { data := m.curEncryptionKey.toArray }) ByteArray.empty 32)[i]!

def Cryptlib.Protocols.BACAP.Ratchet.advanceOne (m : Types.MessageBoxIndex) (hkdf : Primitives.Hash.HKDF.HKDF) : Types.MessageBoxIndex

Advance one step: expand HKDF(IKM=H_i, info=idx64 LE) to 96 bytes, split as H_{i+1} ‖ E ‖ K, and increment idx64.

Equations

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

def Cryptlib.Protocols.BACAP.Ratchet.advanceTo (m : Types.MessageBoxIndex) (hkdf : Primitives.Hash.HKDF.HKDF) (target : UInt64) : Option Types.MessageBoxIndex

Advance to target; none if target is behind the current index.

Equations

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

def Cryptlib.Protocols.BACAP.Ratchet.advanceTo.go (hkdf : Primitives.Hash.HKDF.HKDF) (target : UInt64) : ℕ → Types.MessageBoxIndex → Types.MessageBoxIndex

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.BACAP.Ratchet.advanceTo.go hkdf target 0 a✝ = a✝

def Cryptlib.Protocols.BACAP.Ratchet.nextIndex (m : Types.MessageBoxIndex) (hkdf : Primitives.Hash.HKDF.HKDF) : Option Types.MessageBoxIndex

Advance the ratchet by one step.

Equations

• Cryptlib.Protocols.BACAP.Ratchet.nextIndex m hkdf = Cryptlib.Protocols.BACAP.Ratchet.advanceTo m hkdf (m.idx64 + 1)

def Cryptlib.Protocols.BACAP.Ratchet.mutateKDFStateLabel : ByteArray

HKDF info label separating mutateKDFState from ordinary advancement.

Equations

• Cryptlib.Protocols.BACAP.Ratchet.mutateKDFStateLabel = "bacap-mutate-kdf-state-v1".toUTF8

def Cryptlib.Protocols.BACAP.Ratchet.mutateKDFState (m : Types.MessageBoxIndex) (hkdf : Primitives.Hash.HKDF.HKDF) (ctx : ByteArray) : Types.MessageBoxIndex

Re-seed the ratchet state from ctx, preserving idx64 and the root key. The result addresses a fresh box sequence that cannot be found without ctx.

Equations

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

def Cryptlib.Protocols.BACAP.Ratchet.ofRandomBytes (rb : Vector UInt8 48) (hkdf : Primitives.Hash.HKDF.HKDF) : Types.MessageBoxIndex

A fresh MessageBoxIndex from 48 random bytes: 32 bytes of HKDF state, and a starting index that is the sum of two 62-bit little-endian draws, then advanced once. A random start hides how many messages precede a shared capability.

Equations

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

theorem Cryptlib.Protocols.BACAP.Ratchet.mutateKDFState_preserves_idx64 (m : Types.MessageBoxIndex) (hkdf : Primitives.Hash.HKDF.HKDF) (ctx : ByteArray) : (mutateKDFState m hkdf ctx).idx64 = m.idx64

mutateKDFState preserves idx64.

theorem Cryptlib.Protocols.BACAP.Ratchet.advanceOne_increments_idx64 (m : Types.MessageBoxIndex) (hkdf : Primitives.Hash.HKDF.HKDF) : (advanceOne m hkdf).idx64 = m.idx64 + 1

theorem Cryptlib.Protocols.BACAP.Ratchet.advanceTo_noop (m : Types.MessageBoxIndex) (hkdf : Primitives.Hash.HKDF.HKDF) : advanceTo m hkdf m.idx64 = some m