BACAP API over BLAKE2b-512 HKDF and AES-256-GCM-SIV

Stateless: callers hold their own index. Operations take capabilities rather than loose keys, so pk = publicKey sk holds by construction.

MessageBoxIndex: ratchet advancement

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.advanceIndexTo (m : MessageBoxIndex) (target : UInt64) : Option MessageBoxIndex

Advance the ratchet to target, or none if that would rewind.

Equations

• m.advanceIndexTo target = Cryptlib.Protocols.BACAP.Ratchet.advanceTo m Cryptlib.Primitives.Hash.HKDF.blake2b512_hkdf target

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.nextIndex (m : MessageBoxIndex) : Option MessageBoxIndex

Equations

• m.nextIndex = Cryptlib.Protocols.BACAP.Ratchet.nextIndex m Cryptlib.Primitives.Hash.HKDF.blake2b512_hkdf

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.mutateKDFState (m : MessageBoxIndex) (ctx : ByteArray) : MessageBoxIndex

See Ratchet.mutateKDFState.

Equations

• m.mutateKDFState ctx = Cryptlib.Protocols.BACAP.Ratchet.mutateKDFState m Cryptlib.Primitives.Hash.HKDF.blake2b512_hkdf ctx

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.random (rb : Vector UInt8 48) : MessageBoxIndex

See Ratchet.ofRandomBytes.

Equations

• Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.random rb = Cryptlib.Protocols.BACAP.Ratchet.ofRandomBytes rb Cryptlib.Primitives.Hash.HKDF.blake2b512_hkdf

MessageBoxIndex: box IDs

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.deriveMessageBoxID (m : MessageBoxIndex) (rootPublicKey : Primitives.Sign.Ed25519Blinded.PubBytes) : Primitives.Sign.Ed25519Blinded.PubBytes

Box ID for this index under rootPublicKey, with no context applied.

Equations

• m.deriveMessageBoxID rootPublicKey = Cryptlib.Protocols.BACAP.Impl.implDeriveMessageBoxID rootPublicKey m

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.boxIDForContext (m : MessageBoxIndex) (rc : ReadCap) (ctx : ByteArray) : Primitives.Sign.Ed25519Blinded.PubBytes

Box ID for this index and ctx.

Equations

• m.boxIDForContext rc ctx = Cryptlib.Protocols.BACAP.Impl.implDeriveBoxID rc.rootPublicKey m ctx

MessageBoxIndex: sign, verify, encrypt, decrypt

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.signBox (m : MessageBoxIndex) (owner : WriteCap) (ctx ciphertext : ByteArray) : Primitives.Sign.Ed25519Blinded.PubBytes × Primitives.Sign.Ed25519Blinded.SigBytes

Sign ciphertext with the blinded key for this index and ctx; returns (box ID, signature). The signature is plain Ed25519 under the box ID.

Equations

• m.signBox owner ctx ciphertext = Cryptlib.Protocols.BACAP.Impl.implSignBox owner.rootPrivateKey m ctx ciphertext

def Cryptlib.Protocols.BACAP.Types.verifyBox (box : Primitives.Sign.Ed25519Blinded.PubBytes) (ciphertext : ByteArray) (sig : Primitives.Sign.Ed25519Blinded.SigBytes) : Bool

Verify a signature under a box ID.

Equations

• Cryptlib.Protocols.BACAP.Types.verifyBox box ciphertext sig = Cryptlib.Protocols.BACAP.Impl.implVerifyBox box ciphertext sig

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.encryptForContext (m : MessageBoxIndex) (owner : WriteCap) (ctx plaintext : ByteArray) : Primitives.Sign.Ed25519Blinded.PubBytes × ByteArray × Primitives.Sign.Ed25519Blinded.SigBytes

Returns (box ID, ciphertext, signature). The box ID's first 12 bytes are the AEAD nonce; all 32 bytes are the AD.

Equations

• m.encryptForContext owner ctx plaintext = Cryptlib.Protocols.BACAP.Impl.implEncryptBox owner.rootPrivateKey owner.rootPublicKey m ctx plaintext

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.decryptForContext (m : MessageBoxIndex) (box : Primitives.Sign.Ed25519Blinded.PubBytes) (ctx ciphertext : ByteArray) (sig : Primitives.Sign.Ed25519Blinded.SigBytes) : Option ByteArray

Verify the signature, then decrypt. A tombstone (empty ciphertext) decrypts to empty.

Equations

• m.decryptForContext box ctx ciphertext sig = Cryptlib.Protocols.BACAP.Impl.implDecryptBox box m ctx ciphertext sig

Capabilities

def Cryptlib.Protocols.BACAP.Types.WriteCap.deriveBoxID (wc : WriteCap) (idx : MessageBoxIndex) : Primitives.Sign.Ed25519Blinded.PubBytes

Box ID for idx under this cap's root key, with no context applied.

Equations

• wc.deriveBoxID idx = Cryptlib.Protocols.BACAP.Impl.implDeriveMessageBoxID wc.rootPublicKey idx

def Cryptlib.Protocols.BACAP.Types.ReadCap.deriveBoxID (rc : ReadCap) (idx : MessageBoxIndex) : Primitives.Sign.Ed25519Blinded.PubBytes

Box ID for idx under this cap's root key, with no context applied.

Equations

• rc.deriveBoxID idx = Cryptlib.Protocols.BACAP.Impl.implDeriveMessageBoxID rc.rootPublicKey idx

def Cryptlib.Protocols.BACAP.Types.WriteCap.mutateKDFState (wc : WriteCap) (ctx : ByteArray) : WriteCap

Re-seed this cap's index from ctx.

Equations

• wc.mutateKDFState ctx = { rootSeed := wc.rootSeed, messageBoxIndex := wc.messageBoxIndex.mutateKDFState ctx }

def Cryptlib.Protocols.BACAP.Types.ReadCap.mutateKDFState (rc : ReadCap) (ctx : ByteArray) : ReadCap

Re-seed this cap's index from ctx.

Equations

• rc.mutateKDFState ctx = { rootPublicKey := rc.rootPublicKey, messageBoxIndex := rc.messageBoxIndex.mutateKDFState ctx }

theorem Cryptlib.Protocols.BACAP.Types.readCap_mutateKDFState (wc : WriteCap) (ctx : ByteArray) : wc.readCap.mutateKDFState ctx = (wc.mutateKDFState ctx).readCap

Mutating a write cap and its read cap by the same context lands them on the same sequence.

Key generation from the system CSPRNG

def Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.randomIO : IO MessageBoxIndex

Equations

• Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.randomIO = do let __do_lift ← Cryptlib.Protocols.BACAP.Types.randomVector✝ 48 pure (Cryptlib.Protocols.BACAP.Types.MessageBoxIndex.random __do_lift)

def Cryptlib.Protocols.BACAP.Types.WriteCap.generate : IO WriteCap

A fresh root keypair and starting index.

Equations

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

Correctness

theorem Cryptlib.Protocols.BACAP.Types.writeCap_pub (wc : WriteCap) : wc.rootPublicKey = Primitives.Sign.Ed25519Blinded.publicKey wc.rootPrivateKey

A cap's public key is the one its private key derives.

theorem Cryptlib.Protocols.BACAP.Types.decrypt_encryptForContext (wc : WriteCap) (m : MessageBoxIndex) (ctx pt : ByteArray) : m.decryptForContext (m.encryptForContext wc ctx pt).1 ctx (m.encryptForContext wc ctx pt).2.1 (m.encryptForContext wc ctx pt).2.2 = some pt

Decrypting a box encrypted under the same cap, index and context returns the plaintext.