BACAP types: MessageBoxIndex, ReadCap, WriteCap (Echomix §4)

Binary layouts:

• MessageBoxIndex: uint64 LE ++ [32]byte ++ [32]byte ++ [32]byte = 104 bytes
• ReadCap: [32]byte pubkey ++ MessageBoxIndex = 136 bytes
• WriteCap: [32]byte seed ++ [32]byte pubkey ++ MessageBoxIndex = 168 bytes

@[reducible, inline]

abbrev Cryptlib.Protocols.BACAP.Types.MessageBoxIndexSize : ℕ

Equations

• Cryptlib.Protocols.BACAP.Types.MessageBoxIndexSize = 104

@[reducible, inline]

abbrev Cryptlib.Protocols.BACAP.Types.ReadCapSize : ℕ

Equations

• Cryptlib.Protocols.BACAP.Types.ReadCapSize = 136

@[reducible, inline]

abbrev Cryptlib.Protocols.BACAP.Types.WriteCapSize : ℕ

Equations

• Cryptlib.Protocols.BACAP.Types.WriteCapSize = 168

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

Ratchet state: message counter, blinding factor K_i, encryption key E_i, HKDF state H_i.

• idx64 : UInt64
• curBlindingFactor : Vector UInt8 32
• curEncryptionKey : Vector UInt8 32
• hkdfState : Vector UInt8 32

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.empty : MessageBoxIndex

Equations

• Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.empty = { idx64 := 0, curBlindingFactor := Vector.replicate 32 0, curEncryptionKey := Vector.replicate 32 0, hkdfState := Vector.replicate 32 0 }

@[instance_reducible]

instance Cryptlib.Protocols.BACAP.Types.instInhabitedMessageBoxIndex : Inhabited MessageBoxIndex

Equations

• Cryptlib.Protocols.BACAP.Types.instInhabitedMessageBoxIndex = { default := Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.empty }

def Cryptlib.Protocols.BACAP.Types.marshalMessageBoxIndex (m : MessageBoxIndex) : Vector UInt8 MessageBoxIndexSize

Equations

• Cryptlib.Protocols.BACAP.Types.marshalMessageBoxIndex m = Cryptlib.Protocols.BACAP.Types.putU64LE✝ m.idx64 ++ m.curBlindingFactor ++ m.curEncryptionKey ++ m.hkdfState

def Cryptlib.Protocols.BACAP.Types.unmarshalMessageBoxIndex (data : Vector UInt8 MessageBoxIndexSize) : MessageBoxIndex

Equations

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

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

• rootPublicKey : Vector UInt8 32
• messageBoxIndex : MessageBoxIndex

def Cryptlib.Protocols.BACAP.Types.marshalReadCap (rc : ReadCap) : Vector UInt8 ReadCapSize

Equations

• Cryptlib.Protocols.BACAP.Types.marshalReadCap rc = rc.rootPublicKey ++ Cryptlib.Protocols.BACAP.Types.marshalMessageBoxIndex rc.messageBoxIndex

def Cryptlib.Protocols.BACAP.Types.unmarshalReadCap (data : Vector UInt8 ReadCapSize) : Option ReadCap

Deserialize pubkey ++ index; none if the root public key is not an edwards25519 point (an unreduced y is accepted).

Equations

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

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

A write capability: the root Ed25519 seed plus the earliest reachable index. The seed is kept because the expanded scalar clamp(SHA-512(seed)) cannot be inverted for serialization.

• rootSeed : Vector UInt8 32
• messageBoxIndex : MessageBoxIndex

def Cryptlib.Protocols.BACAP.Types.WriteCap.rootPrivateKey (wc : WriteCap) : Primitives.Sign.Ed25519Blinded.Scalar

The root signing scalar S_R, expanded from the seed per RFC 8032.

Equations

• wc.rootPrivateKey = Cryptlib.Primitives.Sign.Ed25519Blinded.scalarFromSeed wc.rootSeed

def Cryptlib.Protocols.BACAP.Types.WriteCap.rootPublicKey (wc : WriteCap) : Primitives.Sign.Ed25519Blinded.PubBytes

The root verification key P_R = S_R · G.

Equations

• wc.rootPublicKey = Cryptlib.Primitives.Sign.Ed25519Blinded.publicKey wc.rootPrivateKey

def Cryptlib.Protocols.BACAP.Types.WriteCap.readCap (wc : WriteCap) : ReadCap

The read capability at the same index: derives and decrypts the same boxes, cannot sign.

Equations

• wc.readCap = { rootPublicKey := wc.rootPublicKey, messageBoxIndex := wc.messageBoxIndex }

def Cryptlib.Protocols.BACAP.Types.WriteCap.withMessageBoxIndex (wc : WriteCap) (idx : MessageBoxIndex) : WriteCap

Re-base the cap to idx. The holder of the result learns nothing about earlier indices.

Equations

• wc.withMessageBoxIndex idx = { rootSeed := wc.rootSeed, messageBoxIndex := idx }

def Cryptlib.Protocols.BACAP.Types.ReadCap.withMessageBoxIndex (rc : ReadCap) (idx : MessageBoxIndex) : ReadCap

Re-base the cap to idx. The holder of the result learns nothing about earlier indices.

Equations

• rc.withMessageBoxIndex idx = { rootPublicKey := rc.rootPublicKey, messageBoxIndex := idx }

def Cryptlib.Protocols.BACAP.Types.marshalWriteCap (wc : WriteCap) : Vector UInt8 WriteCapSize

Serialize as seed ++ pubkey ++ index.

Equations

• Cryptlib.Protocols.BACAP.Types.marshalWriteCap wc = wc.rootSeed ++ wc.rootPublicKey ++ Cryptlib.Protocols.BACAP.Types.marshalMessageBoxIndex wc.messageBoxIndex

def Cryptlib.Protocols.BACAP.Types.unmarshalWriteCap (data : Vector UInt8 WriteCapSize) : Option WriteCap

Deserialize seed ++ pubkey ++ index; none if the stored public key is not the one the seed derives.

Equations

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

unmarshal ∘ marshal is the identity

@[simp]

theorem Cryptlib.Protocols.BACAP.Types.unmarshal_marshal_messageBoxIndex (m : MessageBoxIndex) : unmarshalMessageBoxIndex (marshalMessageBoxIndex m) = m

theorem Cryptlib.Protocols.BACAP.Types.unmarshal_marshal_readCap (rc : ReadCap) (h : (Primitives.Sign.Ed25519Math.decodePoint rc.rootPublicKey).isSome = true) : unmarshalReadCap (marshalReadCap rc) = some rc

A read cap whose root public key is a curve point round-trips.

@[simp]

theorem Cryptlib.Protocols.BACAP.Types.unmarshal_marshal_writeCap (wc : WriteCap) : unmarshalWriteCap (marshalWriteCap wc) = some wc

Every write cap round-trips.

marshal ∘ unmarshal is the identity on blobs that parse: encodings are canonical

@[simp]

theorem Cryptlib.Protocols.BACAP.Types.marshal_unmarshal_messageBoxIndex (d : Vector UInt8 MessageBoxIndexSize) : marshalMessageBoxIndex (unmarshalMessageBoxIndex d) = d

theorem Cryptlib.Protocols.BACAP.Types.marshal_unmarshal_readCap {data : Vector UInt8 ReadCapSize} {rc : ReadCap} (h : unmarshalReadCap data = some rc) : marshalReadCap rc = data

A read cap that parses re-serializes to the bytes it came from.

theorem Cryptlib.Protocols.BACAP.Types.marshal_unmarshal_writeCap {data : Vector UInt8 WriteCapSize} {wc : WriteCap} (h : unmarshalWriteCap data = some wc) : marshalWriteCap wc = data

A write cap that parses re-serializes to the bytes it came from.