Perfect Secrecy: Definitions

Core definitions for perfect secrecy following [KL20], Chapter 2.

Main definitions

• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.ciphertextDist: ciphertext distribution for a given message
• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.jointDist: joint (message, ciphertext) distribution given a message prior
• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.marginalCiphertextDist: marginal ciphertext distribution given a message prior
• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.posteriorMsgDist: posterior message distribution Pr[M | C = c] as a PMF
• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.PerfectlySecret: perfect secrecy ([KL20], Definition 2.3)
• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.CiphertextIndist: ciphertext indistinguishability ([KL20], Lemma 2.5)

noncomputable def Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.ciphertextDist {M K C : Type u} (scheme : EncScheme M K C) (m : M) : PMF C

The distribution of Enc_K(m) when K ← Gen.

Equations

• scheme.ciphertextDist m = do let __do_lift ← scheme.gen scheme.enc __do_lift m

noncomputable def Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.jointDist {M K C : Type u} (scheme : EncScheme M K C) (msgDist : PMF M) : PMF (M × C)

Joint distribution of (M, C) given a message prior.

Equations

• scheme.jointDist msgDist = do let m ← msgDist let __do_lift ← scheme.ciphertextDist m pure (m, __do_lift)

noncomputable def Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.marginalCiphertextDist {M K C : Type u} (scheme : EncScheme M K C) (msgDist : PMF M) : PMF C

Marginal ciphertext distribution given a message prior.

Equations

• scheme.marginalCiphertextDist msgDist = do let __do_lift ← msgDist scheme.ciphertextDist __do_lift

noncomputable def Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.posteriorMsgDist {M K C : Type u} (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) : PMF M

The posterior message distribution Pr[M | C = c] as a probability distribution, given a message prior and a ciphertext in the support of the marginal distribution.

Equations

• scheme.posteriorMsgDist msgDist c hc = Cslib.Probability.PMF.posteriorDist msgDist scheme.ciphertextDist c hc

@[simp]

theorem Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.posteriorMsgDist_apply {M K C : Type u} (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) (m : M) : (scheme.posteriorMsgDist msgDist c hc) m = (scheme.jointDist msgDist) (m, c) / (scheme.marginalCiphertextDist msgDist) c

def Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.PerfectlySecret {M K C : Type u} (scheme : EncScheme M K C) : Prop

An encryption scheme is perfectly secret if the posterior message distribution equals the prior for every ciphertext with positive probability ([KL20], Definition 2.3).

Equations

• scheme.PerfectlySecret = ∀ (msgDist : PMF M) (c : C) (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support), scheme.posteriorMsgDist msgDist c hc = msgDist

def Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.CiphertextIndist {M K C : Type u} (scheme : EncScheme M K C) : Prop

Ciphertext indistinguishability: the ciphertext distribution is the same for all messages ([KL20], Lemma 2.5).

Equations

• scheme.CiphertextIndist = ∀ (m₀ m₁ : M), scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁