Symmetric Encryption Schemes.

This file defines a type SymmEncAlg spec M K C to represent a protocol for symmetric encryption using oracles in spec, with message space M, secret keys of type K, and ciphertext space C.

structure SymmEncAlg (m : Type u → Type v) (M K C : Type u) extends ExecutionMethod m : Type (max (u + 1) v)

Symmetric encryption algorithm with access to oracles in spec (simulated with state σ), where M is the space of messages, K is the key space, and C is the ciphertext space.

• exec {α : Type u} : m α → ProbComp α
• lift_probComp {α : Type u} : ProbComp α → m α
• exec_lift_probComp {α : Type u} (px : ProbComp α) : self.exec (self.lift_probComp px) = px
• keygen : m K
• encrypt (k : K) (msg : M) : m C
• decrypt (k : K) (c : C) : Option M

class SymmEncAlg.Complete {m : Type → Type v} {M K C : Type} [AlternativeMonad m] (encAlg : SymmEncAlg m M K C) : Prop

A SymmEncAlg is complete if decrypting an encrypted message always returns that original message, captured here by a guard statement.

TODO: should this be a class?

• decrypt_encrypt_eq_message (msg : M) : [=some msg|encAlg.exec do let k ← encAlg.keygen let __do_lift ← encAlg.encrypt k msg pure (encAlg.decrypt k __do_lift)] = 1

def SymmEncAlg.perfectSecrecy {m : Type → Type v} {M K C : Type} [AlternativeMonad m] (encAlg : SymmEncAlg m M K C) : Prop

theorem SymmEncAlg.perfectSecrecy_iff_of_card_eq {m : Type → Type v} {M K C : Type} [AlternativeMonad m] [LawfulAlternative m] [Fintype M] [Fintype K] [Fintype C] (encAlg : SymmEncAlg m M K C) [encAlg.Complete] (h1 : Fintype.card M = Fintype.card K) (h2 : Fintype.card K = Fintype.card C) : encAlg.perfectSecrecy ↔ (∀ (k : K), [=k|encAlg.exec encAlg.keygen] = (↑(Fintype.card K))⁻¹) ∧ ∀ (m_1 : M) (c : m C), ∃! k : K, k ∈ OracleComp.support (encAlg.exec encAlg.keygen) ∧ encAlg.encrypt k m_1 = c

Shanon's theorem on perfect secrecy, showing that encryption and decryption must be determined bijections between message and cipher-text space, and that keys must be chosen uniformly.