Private-Key Encryption Schemes (Information-Theoretic)

An information-theoretic private-key encryption scheme following [KL20], Definition 2.1. Key generation and encryption are probability distributions over arbitrary types, with no computational constraints.

Main definitions

• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme: a private-key encryption scheme (Gen, Enc, Dec) with correctness

References

• J. Katz, Y. Lindell, Introduction to Modern Cryptography

structure Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme (Message : Type u_1) (Key : Type u_2) (Ciphertext : Type u_3) : Type (max (max u_1 u_2) u_3)

A private-key encryption scheme over message space M, key space K, and ciphertext space C ([KL20], Definition 2.1).

• gen : PMF Key

  Probabilistic key generation.

• enc (key : Key) (message : Message) : PMF Ciphertext

  (Possibly randomized) encryption.

• dec (key : Key) (ciphertext : Ciphertext) : Message

  Deterministic decryption.

• correct (key : Key) : key ∈ self.gen.support → ∀ (message : Message), ∀ ciphertext ∈ (self.enc key message).support, self.dec key ciphertext = message

  Decryption inverts encryption for all keys in the support of gen.

noncomputable def Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.ofPure {Message Key Ciphertext : Type u} (gen : PMF Key) (enc : Key → Message → Ciphertext) (dec : Key → Ciphertext → Message) (h : ∀ (key : Key), Function.LeftInverse (dec key) (enc key)) : EncScheme Message Key Ciphertext

Build an encryption scheme from deterministic pure encryption/decryption where decryption is a left inverse of encryption for every key.

Equations

• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.ofPure gen enc dec h = { gen := gen, enc := fun (key : Key) (message : Message) => PMF.pure (enc key message), dec := dec, correct := ⋯ }