Helper

enc_mul_dist

Section paillier_params

Type Lemma

Proof Lines 8

Lemma enc_mul_dist : forall (m1 m2 : 'Z_n) (r1 r2 : {unit 'Z_n2}), paillier_enc m1 r1 * paillier_enc m2 r2 = paillier_enc (m1 + m2) (r1 * r2)%g.

Encryption multiplication distributes as addition on messages

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

No lemmas in the stats use this lemma.

Loading source code...