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 K C : ℕ → Type) (Q : Type v) extends OracleContext Q ProbComp : Type (v + 1)

• spec : OracleSpec Q
• impl : QueryImpl self.spec ProbComp
• keygen (sp : ℕ) : OracleComp self.spec (K sp)
• encrypt {sp : ℕ} (k : K sp) (msg : M sp) : OracleComp self.spec (C sp)
• decrypt {sp : ℕ} (k : K sp) (c : C sp) : OptionT (OracleComp self.spec) (M sp)

def SymmEncAlg.CompleteExp {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) {sp : ℕ} (m : M sp) : OptionT (OracleComp encAlg.spec) (M sp)

def SymmEncAlg.Complete {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) : Prop

def SymmEncAlg.perfectSecrecy {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) : Prop