Helper

E_enc_ce_contract

File homomorphic_encryption/homomorphic_encryption.v

Section enc_lemmas

Type Lemma

Proof Lines 25

Signature

Lemma E_enc_ce_contract (A B C : finType) (p : party_id) (X : {RV P -> A})(E : {RV P -> p.-enc B})(Z : {RV P -> C})(n : nat): #|B| = n.+1 -> (forall x e, `Pr[ [%X, E] = (x, e)] != 0) -> `H(Z | [%X, E]) = `H(Z | X).

Description

"Ciphertext conditioning contract": if `E` is a fresh encryption value (uniform over `p.-enc B` and independent from everything else), then conditioning on `E` does not change the conditional entropy of `Z` given `X`. The hypothesis `(forall x e, Pr[[X,E]=(x,e)] != 0)` is a technical condition to make all the conditional probabilities `Pr[ Z=c | [X,E]=(x,e) ]` well-defined in the cpr/centropy lemmas used below.

Uses (0)

This lemma does not use any other lemmas from the stats.

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats