Main

paillier_dec_correct

Section paillier_params

Type Lemma

Proof Lines 10

Lemma paillier_dec_correct (m : 'Z_n) (r : {unit 'Z_n2}) : paillier_dec lambda (paillier_enc m r) = Some m.

Decryption with the canonical key recovers the original message

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

No lemmas in the stats use this lemma.

Loading source code...