Encryption Scheme Definition

This file defines the structure of symmetric encryption schemes for use in cryptographic security proofs.

Main definitions

• EncScheme - A symmetric encryption scheme with key generation, encryption, and decryption
• EncScheme.Correct - Correctness property: decryption inverts encryption
• EncScheme.IsDeterministic - Predicate for deterministic encryption
• ProbEncScheme - Probabilistic encryption with explicit randomness
• DetEncScheme - Deterministic encryption scheme

References

• [Bellare & Rogaway, Introduction to Modern Cryptography]
• [Katz & Lindell, Introduction to Modern Cryptography]

structure CatCrypt.Crypto.EncScheme : Type 1

A symmetric encryption scheme.

An encryption scheme consists of:

• Key, Plaintext, and Ciphertext types
• A probabilistic key generation algorithm
• A probabilistic encryption algorithm
• A probabilistic decryption algorithm

The type requirements (Fintype, Nonempty) are needed for:

• Key: uniform sampling in key generation
• Ciphertext: supporting one-time pad style encryption where ciphertexts are sampled/XORed with keys

Note: Decryption returns Option Plaintext to handle decryption failures (e.g., authenticated encryption modes).

• Key : Type

  Key type

• Plaintext : Type

  Plaintext type

• Ciphertext : Type

  Ciphertext type

• finKey : Fintype self.Key

  Keys form a finite type (for uniform sampling)

• neKey : Nonempty self.Key

  Keys are nonempty (for uniform sampling)

• finCt : Fintype self.Ciphertext

  Ciphertexts form a finite type (for OTP-style constructions)

• neCt : Nonempty self.Ciphertext

  Ciphertexts are nonempty (for OTP-style constructions)

• keyGen : Core.SPComp self.Key

  Probabilistic key generation

• encrypt : self.Key → self.Plaintext → Core.SPComp self.Ciphertext

  Probabilistic encryption

• decrypt : self.Key → self.Ciphertext → Core.SPComp (Option self.Plaintext)

  Probabilistic decryption (may fail)

Correctness Property

def CatCrypt.Crypto.EncScheme.Correct (E : EncScheme) : Prop

Correctness: decryption of encryption returns the original message.

For a deterministic scheme, this means: ∀ k m, decrypt k (encrypt k m) = some m

For probabilistic schemes, we require that for any randomness used in encryption, decryption recovers the original message. We express this using support membership.

Note: This requires that for all ciphertexts c in the support of encrypt k m, decryption returns some m.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Crypto.EncScheme.StrongCorrect (E : EncScheme) : Prop

Strong correctness: decryption always succeeds and returns original message. This is expressed as equality of distributions after bind.

Equations

• One or more equations did not get rendered due to their size.

Determinism

def CatCrypt.Crypto.EncScheme.IsDeterministic (E : EncScheme) : Prop

Deterministic encryption: encrypt is a pure function of key and message. The encryption produces a single deterministic ciphertext.

Equations

• E.IsDeterministic = ∃ (f : E.Key → E.Plaintext → E.Ciphertext), ∀ (k : E.Key) (m : E.Plaintext), E.encrypt k m = CatCrypt.Core.SPComp.pure (f k m)

def CatCrypt.Crypto.EncScheme.HasDeterministicDecrypt (E : EncScheme) : Prop

Deterministic decryption: decrypt is a pure function of key and ciphertext.

Equations

• E.HasDeterministicDecrypt = ∃ (f : E.Key → E.Ciphertext → Option E.Plaintext), ∀ (k : E.Key) (c : E.Ciphertext), E.decrypt k c = CatCrypt.Core.SPComp.pure (f k c)

def CatCrypt.Crypto.EncScheme.IsFullyDeterministic (E : EncScheme) : Prop

A fully deterministic scheme has both deterministic encryption and decryption.

Equations

• E.IsFullyDeterministic = (E.IsDeterministic ∧ E.HasDeterministicDecrypt)

Simple Correctness for Deterministic Schemes

def CatCrypt.Crypto.EncScheme.SimpleCorrect (E : EncScheme) (encryptF : E.Key → E.Plaintext → E.Ciphertext) (decryptF : E.Key → E.Ciphertext → Option E.Plaintext) : Prop

Simple correctness condition for schemes with deterministic encrypt/decrypt. This is easier to prove and implies the general Correct property.

Equations

• E.SimpleCorrect encryptF decryptF = ∀ (k : E.Key) (m : E.Plaintext), decryptF k (encryptF k m) = some m

theorem CatCrypt.Crypto.EncScheme.correct_of_simple_correct (E : EncScheme) (encryptF : E.Key → E.Plaintext → E.Ciphertext) (decryptF : E.Key → E.Ciphertext → Option E.Plaintext) (hEnc : ∀ (k : E.Key) (m : E.Plaintext), E.encrypt k m = Core.SPComp.pure (encryptF k m)) (hDec : ∀ (k : E.Key) (c : E.Ciphertext), E.decrypt k c = Core.SPComp.pure (decryptF k c)) (hSimple : E.SimpleCorrect encryptF decryptF) : E.Correct

If a scheme has deterministic encrypt/decrypt satisfying SimpleCorrect, then it satisfies the general Correct property.

Deterministic Encryption Scheme

structure CatCrypt.Crypto.DetEncScheme : Type 1

A deterministic encryption scheme where encryption and decryption are pure functions. This is a special case useful for schemes like OTP, block ciphers, etc.

• Key : Type

  Key type

• Plaintext : Type

  Plaintext type

• Ciphertext : Type

  Ciphertext type

• finKey : Fintype self.Key

  Keys form a finite type (for uniform sampling)

• neKey : Nonempty self.Key

  Keys are nonempty (for uniform sampling)

• finCt : Fintype self.Ciphertext

  Ciphertexts form a finite type

• neCt : Nonempty self.Ciphertext

  Ciphertexts are nonempty

• encryptF : self.Key → self.Plaintext → self.Ciphertext

  Deterministic encryption function

• decryptF : self.Key → self.Ciphertext → Option self.Plaintext

  Deterministic decryption function

noncomputable def CatCrypt.Crypto.DetEncScheme.toEncScheme (D : DetEncScheme) : EncScheme

Convert a deterministic scheme to a general encryption scheme.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Crypto.DetEncScheme.Correct (D : DetEncScheme) : Prop

Correctness for deterministic schemes: decrypt inverts encrypt.

Equations

• D.Correct = ∀ (k : D.Key) (m : D.Plaintext), D.decryptF k (D.encryptF k m) = some m

def CatCrypt.Crypto.DetEncScheme.EncryptInjective (D : DetEncScheme) : Prop

Encryption is injective in the message for each key.

Equations

• D.EncryptInjective = ∀ (k : D.Key) (m₁ m₂ : D.Plaintext), D.encryptF k m₁ = D.encryptF k m₂ → m₁ = m₂

theorem CatCrypt.Crypto.DetEncScheme.encrypt_injective_of_correct (D : DetEncScheme) (hCorr : D.Correct) : D.EncryptInjective

Correctness implies encryption is injective.

theorem CatCrypt.Crypto.DetEncScheme.toEncScheme_correct (D : DetEncScheme) (hCorr : D.Correct) : D.toEncScheme.Correct

A correct deterministic scheme gives a correct general scheme.

Probabilistic Encryption Scheme with Explicit Randomness

structure CatCrypt.Crypto.ProbEncSchemeextends CatCrypt.Crypto.EncScheme : Type 1

A probabilistic encryption scheme with explicit randomness. This models schemes like ElGamal, RSA-OAEP, etc. where encryption uses random coins that can be made explicit.

• Key : Type
• Plaintext : Type
• Ciphertext : Type
• finKey : Fintype self.Key
• neKey : Nonempty self.Key
• finCt : Fintype self.Ciphertext
• neCt : Nonempty self.Ciphertext
• keyGen : Core.SPComp self.Key
• encrypt : self.Key → self.Plaintext → Core.SPComp self.Ciphertext
• decrypt : self.Key → self.Ciphertext → Core.SPComp (Option self.Plaintext)
• Randomness : Type

  Randomness type used in encryption

• finRand : Fintype self.Randomness

  Randomness is finite (for uniform sampling)

• neRand : Nonempty self.Randomness

  Randomness is nonempty

• encryptR : self.Key → self.Plaintext → self.Randomness → self.Ciphertext

  Deterministic encryption with explicit randomness

• encrypt_eq (k : self.Key) (m : self.Plaintext) : self.encrypt k m = do let r ← Core.SPComp.sample self.Randomness Core.SPComp.pure (self.encryptR k m r)

  Probabilistic encryption samples randomness and applies encryptR

def CatCrypt.Crypto.ProbEncScheme.Correct (P : ProbEncScheme) : Prop

Correctness for probabilistic schemes: for all randomness, decrypt recovers message. This uses the base scheme's Correct property specialized to the encrypted ciphertext.

Equations

• P.Correct = P.Correct

def CatCrypt.Crypto.ProbEncScheme.SimpleCorrect (P : ProbEncScheme) (decryptF : P.Key → P.Ciphertext → Option P.Plaintext) : Prop

Simple correctness when decryption is also deterministic.

Equations

• P.SimpleCorrect decryptF = ∀ (k : P.Key) (m : P.Plaintext) (r : P.Randomness), decryptF k (P.encryptR k m r) = some m

Basic Lemmas

theorem CatCrypt.Crypto.EncScheme.det_scheme_is_deterministic (D : DetEncScheme) : D.toEncScheme.IsDeterministic

A deterministic scheme is IsDeterministic.

theorem CatCrypt.Crypto.EncScheme.det_scheme_has_det_decrypt (D : DetEncScheme) : D.toEncScheme.HasDeterministicDecrypt

A deterministic scheme has deterministic decryption.

theorem CatCrypt.Crypto.EncScheme.det_scheme_is_fully_deterministic (D : DetEncScheme) : D.toEncScheme.IsFullyDeterministic

A deterministic scheme is fully deterministic.