Multi-recipient KEM

The sender draws an ephemeral key pair, encrypts the payload once under a fresh message key, and encrypts the message key to each recipient under a NIKE shared key (a DEK). A recipient can reply under the same shared key, which the sender reads with the ephemeral private key. The generic construction is MKEMAdapter.mkemOfNike.

Correctness is stated for the ciphertext reduced to one recipient's DEK (forRecipient). Decapsulating the full ciphertext trial-decrypts the DEKs, which is correct only under AEAD authenticity, a computational property. IND-CCA2 and recipient anonymity are likewise not laws. The ciphertext byte encoding is not modelled.

inductive Cryptlib.Primitives.MKEM.MKEM.MKEMError : Type

• unsafePublicKey : MKEMError
• degenerateSharedSecret : MKEMError
• invalidKeySize : MKEMError
• ciphertextTooShort : MKEMError
• trialDecryptFailed : MKEMError

@[instance_reducible]

instance Cryptlib.Primitives.MKEM.MKEM.instDecidableEqMKEMError : DecidableEq MKEMError

Equations

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

structure Cryptlib.Primitives.MKEM.MKEM.Ciphertext (PublicKey : Type) : Type

The ephemeral public key, one DEK per recipient, and the sealed payload.

• ephPub : PublicKey
• deks : List ByteArray
• envelope : ByteArray

def Cryptlib.Primitives.MKEM.MKEM.Ciphertext.forRecipient {PublicKey : Type} (ct : Ciphertext PublicKey) (i : Nat) : Ciphertext PublicKey

The ciphertext with only DEK i.

Equations

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

structure Cryptlib.Primitives.MKEM.MKEM.MKEM : Type 1

• PrivateKey : Type
• PublicKey : Type
• Safe : self.PublicKey → Prop

  Public keys the scheme will compute with, as for NIKE.

• decSafe : DecidablePred self.Safe
• State : Type
• stateI : Inhabited self.State
• name : String
• publicKeySize : 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
• generate : EStateM MKEMError self.State (self.PublicKey × self.PrivateKey)
• encapsulate : List { pk : self.PublicKey // self.Safe pk } → ByteArray → EStateM MKEMError self.State (self.PrivateKey × Ciphertext self.PublicKey)

  Also returns the ephemeral private key, for reading replies.

• decapsulate : self.PrivateKey → Ciphertext self.PublicKey → Except MKEMError ByteArray
• envelopeReply : self.PrivateKey → { pk : self.PublicKey // self.Safe pk } → ByteArray → EStateM MKEMError self.State ByteArray

  A recipient's reply, sealed under its shared key with the sender's ephemeral key.

• decryptEnvelope : self.PrivateKey → { pk : self.PublicKey // self.Safe pk } → ByteArray → Except MKEMError ByteArray
• derive_safe (sk : self.PrivateKey) : self.Safe (self.derivePublicKey sk)
• decode_encode_pub (pk : self.PublicKey) : self.decodePublicKey (self.encodePublicKey pk) = some pk
• generate_derive (s : self.State) (pk : self.PublicKey) (sk : self.PrivateKey) (s' : self.State) : self.generate s = EStateM.Result.ok (pk, sk) s' → pk = self.derivePublicKey sk
• encapsulate_ephPub (keys : List { pk : self.PublicKey // self.Safe pk }) (payload : ByteArray) (s : self.State) (eph : self.PrivateKey) (ct : Ciphertext self.PublicKey) (s' : self.State) : self.encapsulate keys payload s = EStateM.Result.ok (eph, ct) s' → ct.ephPub = self.derivePublicKey eph

  The ciphertext carries the public key of the returned ephemeral private key.

• encapsulate_shape (keys : List { pk : self.PublicKey // self.Safe pk }) (payload : ByteArray) (s : self.State) (eph : self.PrivateKey) (ct : Ciphertext self.PublicKey) (s' : self.State) : self.encapsulate keys payload s = EStateM.Result.ok (eph, ct) s' → ct.deks.length = keys.length ∧ (∀ (d : ByteArray), d ∈ ct.deks → d.size = self.dekSize) ∧ ct.envelope.size = payload.size + self.envelopeOverhead

  One dekSize DEK per recipient, and an envelope envelopeOverhead longer than the payload.

• decapsulate_encapsulate (keys : List { pk : self.PublicKey // self.Safe pk }) (payload : ByteArray) (s : self.State) (eph : self.PrivateKey) (ct : Ciphertext self.PublicKey) (s' : self.State) : self.encapsulate keys payload s = EStateM.Result.ok (eph, ct) s' → ∀ (i : Nat) (hi : i < keys.length) (sk : self.PrivateKey), keys[i] = ⟨self.derivePublicKey sk, ⋯⟩ → self.decapsulate sk (ct.forRecipient i) = Except.ok payload

  Recipient i recovers the payload from ct.forRecipient i.

• decryptEnvelope_envelopeReply (sk eph : self.PrivateKey) (pt : ByteArray) (s : self.State) (env : ByteArray) (s' : self.State) : self.envelopeReply sk ⟨self.derivePublicKey eph, ⋯⟩ pt s = EStateM.Result.ok env s' → self.decryptEnvelope eph ⟨self.derivePublicKey sk, ⋯⟩ env = Except.ok pt

  The sender reads a recipient's reply with the ephemeral private key.