BACAP protocol

Built from a Blindable signature scheme (box IDs), an HKDF (ratchet) and an AEAD (box encryption). Operations are stateless and take a MessageBoxIndex explicitly.

structure Cryptlib.Protocols.BACAP.Protocol.BACAPSpec : Type 1

• blindable : Primitives.Sign.Blindable.Blindable
• hkdf : Primitives.Hash.HKDF.HKDF
• aead : Primitives.Cipher.AEAD.AEAD
• scalarFintype : Fintype self.blindable.Scalar

  Blinding factors can be sampled uniformly.

• scalarSampleable : SampleableType self.blindable.Scalar
• pubDecEq : DecidableEq self.blindable.base.PublicKey
• deriveBoxID : self.blindable.base.PublicKey → Types.MessageBoxIndex → ByteArray → self.blindable.base.PublicKey

  The box ID blindPub(rootPub, K_i^ctx).

• signBox : self.blindable.base.PrivateKey → Types.MessageBoxIndex → ByteArray → ByteArray → self.blindable.base.PublicKey × self.blindable.base.Sig

  Sign a ciphertext with the blinded write key; returns (boxID, signature).

• verifyBox : self.blindable.base.PublicKey → ByteArray → self.blindable.base.Sig → Bool
• encryptBox : self.blindable.base.PrivateKey → self.blindable.base.PublicKey → Types.MessageBoxIndex → ByteArray → ByteArray → self.blindable.base.PublicKey × ByteArray × self.blindable.base.Sig

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

• decryptBox : self.blindable.base.PublicKey → Types.MessageBoxIndex → ByteArray → ByteArray → self.blindable.base.Sig → Option ByteArray

  Verifies the signature first; a tombstone (empty ciphertext) decrypts to empty.

• sign_verify (sk : self.blindable.base.PrivateKey) (idx : Types.MessageBoxIndex) (ctx ct : ByteArray) : let r := self.signBox sk idx ctx ct; self.verifyBox r.1 ct r.2 = true

  A signed ciphertext verifies under the box ID from the same inputs.

• encrypt_boxid (sk : self.blindable.base.PrivateKey) (pk : self.blindable.base.PublicKey) (idx : Types.MessageBoxIndex) (ctx pt : ByteArray) : (self.encryptBox sk pk idx ctx pt).1 = self.deriveBoxID pk idx ctx

  encryptBox writes to the box a reader derives from the root public key.

• encrypt_verify (sk : self.blindable.base.PrivateKey) (pk : self.blindable.base.PublicKey) (idx : Types.MessageBoxIndex) (ctx pt : ByteArray) : pk = self.blindable.base.pub sk → let r := self.encryptBox sk pk idx ctx pt; self.blindable.base.verify r.1 r.2.1 r.2.2 = true

  The signature encryptBox produces verifies under its box ID.

• decrypt_encrypt (sk : self.blindable.base.PrivateKey) (pk : self.blindable.base.PublicKey) (idx : Types.MessageBoxIndex) (ctx pt : ByteArray) : pk = self.blindable.base.pub sk → let r := self.encryptBox sk pk idx ctx pt; self.decryptBox r.1 idx ctx r.2.1 r.2.2 = some pt

  Decrypting an encrypted box returns the plaintext.

• decrypt_sound (sk : self.blindable.base.PrivateKey) (pk boxId : self.blindable.base.PublicKey) (idx : Types.MessageBoxIndex) (ctx ct : ByteArray) (sig : self.blindable.base.Sig) (pt : ByteArray) : pk = self.blindable.base.pub sk → self.deriveBoxID pk idx ctx = boxId → self.decryptBox boxId idx ctx ct sig = some pt → ct.size > 0 → (self.encryptBox sk pk idx ctx pt).2.1 = ct

  A non-tombstone ciphertext that decrypts at the derived box ID is exactly what encryptBox produces for that plaintext.

• unlinkable (pk : self.blindable.base.PublicKey) : self.blindable.Regular pk → ∀ target ∈ Set.range (self.blindable.blindPub pk), Pr[= true | do let f ← $ᵗ self.blindable.Scalar pure (decide (self.blindable.blindPub pk f = target))] = (↑(Fintype.card self.blindable.Scalar))⁻¹

  Unlinkability (Echomix §4.3): for a regular root key pk, a uniform blinding factor yields each key in the orbit of pk with probability 1/|Scalar|.