Multi-recipient hybrid encryption, over a KEM

Like MKEM, but over a KEM, which cannot combine a private key with another party's public key. There is one KEM ciphertext per recipient. The payload is sealed once under a message key, which is wrapped under each recipient's derived key (a DEK). Replies are sealed directly under the derived key, which the sender keeps per recipient and the recipient recovers on decapsulation.

IND-CCA2 and recipient anonymity are computational and not laws. The ciphertext byte encoding is not modelled. The generic construction is Adapter.hybridOfKEM.

inductive Cryptlib.Primitives.MultiRecipientHybrid.MultiRecipientHybrid.MultiRecipientHybridError : Type

decapFailed covers any error from the underlying KEM.decap.

• invalidKeySize : MultiRecipientHybridError
• ciphertextTooShort : MultiRecipientHybridError
• trialDecryptFailed : MultiRecipientHybridError
• decapFailed : MultiRecipientHybridError

@[instance_reducible]

instance Cryptlib.Primitives.MultiRecipientHybrid.MultiRecipientHybrid.instDecidableEqMultiRecipientHybridError : DecidableEq MultiRecipientHybridError

Equations

• Cryptlib.Primitives.MultiRecipientHybrid.MultiRecipientHybrid.instDecidableEqMultiRecipientHybridError x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Cryptlib.Primitives.MultiRecipientHybrid.MultiRecipientHybrid.Ciphertext (KEMCiphertext : Type) : Type

One KEM ciphertext and one DEK per recipient, and the sealed payload.

• kemCiphertexts : List KEMCiphertext
• deks : List ByteArray
• envelope : ByteArray

def Cryptlib.Primitives.MultiRecipientHybrid.MultiRecipientHybrid.Ciphertext.forRecipient {KEMCiphertext : Type} (ct : Ciphertext KEMCiphertext) (i : Nat) : Ciphertext KEMCiphertext

The ciphertext with only recipient i's KEM ciphertext and DEK.

Equations

• ct.forRecipient i = { kemCiphertexts := ct.kemCiphertexts[i]?.toList, deks := ct.deks[i]?.toList, envelope := ct.envelope }

structure Cryptlib.Primitives.MultiRecipientHybrid.MultiRecipientHybrid.MultiRecipientHybrid : Type 1

• PrivateKey : Type
• PublicKey : Type
• KEMCiphertext : Type
• ctI : Inhabited self.KEMCiphertext
• State : Type
• stateI : Inhabited self.State
• name : String
• publicKeySize : Nat
• kemCiphertextSize : Nat
• dekSize : Nat
• envelopeOverhead : Nat
• derivePublicKey : self.PrivateKey → self.PublicKey
• encodePublicKey : self.PublicKey → Vector UInt8 self.publicKeySize
• decodePublicKey : Vector UInt8 self.publicKeySize → Option self.PublicKey
• stateFromSeed : Vector UInt8 32 → self.State
• Reliable : self.State → Prop

  States from which no recipient's encapsulation fails, as KEM.Reliable.

• generate : EStateM MultiRecipientHybridError self.State (self.PublicKey × self.PrivateKey)
• encapsulate : List self.PublicKey → ByteArray → EStateM MultiRecipientHybridError self.State (List ByteArray × Ciphertext self.KEMCiphertext)

  Also returns the per-recipient derived keys, in order, for reading replies.

• decapsulate : self.PrivateKey → Ciphertext self.KEMCiphertext → Except MultiRecipientHybridError (ByteArray × ByteArray)

  Returns the derived key and the payload.

• envelopeReply : ByteArray → ByteArray → EStateM MultiRecipientHybridError self.State ByteArray

  A reply sealed under a derived key.

• decryptEnvelope : ByteArray → ByteArray → Except MultiRecipientHybridError ByteArray
• decode_encode_pub (pk : self.PublicKey) : self.decodePublicKey (self.encodePublicKey pk) = some pk
• encapsulate_shape (keys : List self.PublicKey) (payload : ByteArray) (s : self.State) (derivedKeys : List ByteArray) (ct : Ciphertext self.KEMCiphertext) (s' : self.State) : self.encapsulate keys payload s = EStateM.Result.ok (derivedKeys, ct) s' → ct.kemCiphertexts.length = keys.length ∧ ct.deks.length = keys.length ∧ derivedKeys.length = keys.length ∧ (∀ (d : ByteArray), d ∈ ct.deks → d.size = self.dekSize) ∧ ct.envelope.size = payload.size + self.envelopeOverhead

  One KEM ciphertext, one dekSize DEK and one derived key per recipient, and an envelope envelopeOverhead longer than the payload.

• decapsulate_encapsulate (keys : List self.PublicKey) (payload : ByteArray) (s : self.State) : self.Reliable s → ∀ (derivedKeys : List ByteArray) (ct : Ciphertext self.KEMCiphertext) (s' : self.State), self.encapsulate keys payload s = EStateM.Result.ok (derivedKeys, ct) s' → ∀ (i : Nat) (hi : i < keys.length) (sk : self.PrivateKey) (k : ByteArray), keys[i] = self.derivePublicKey sk → derivedKeys[i]? = some k → self.decapsulate sk (ct.forRecipient i) = Except.ok (k, payload)

  From a Reliable state, recipient i recovers the payload and the sender's derived key k from ct.forRecipient i.

• decryptEnvelope_envelopeReply (key pt : ByteArray) (s : self.State) (env : ByteArray) (s' : self.State) : self.envelopeReply key pt s = EStateM.Result.ok env s' → self.decryptEnvelope key env = Except.ok pt

  Replies round-trip under the same key.