Helper

ciphertext_to_lambda

Section paillier_params

Type Lemma

Proof Lines 6

Lemma ciphertext_to_lambda (m : 'Z_n) (r : {unit 'Z_n2}) : (paillier_enc m r) ^+ lambda = g ^+ (lambda * m).

Raising ciphertext to lambda strips randomness

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

No lemmas in the stats use this lemma.

Loading source code...