Helper

paillier_dec_correct_mixin

File homomorphic_encryption/paillier1999/paillier_ahe.v

Section paillier_instance

Type Lemma

Proof Lines 5

Signature

Lemma paillier_dec_correct_mixin (dk : PaillierPrivKey n) (u : {unit 'Z_n2}) (m : 'Z_n) : paillier_dec_for_mixin dk (paillier_enc_for_mixin (pub_of_priv dk) m u) = Some m.

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