Helper

enc_exp_dist

Section paillier_params

Type Lemma

Proof Lines 9

Lemma enc_exp_dist : forall (m1 : 'Z_n) (m2 : nat) (r : {unit 'Z_n2}), (paillier_enc m1 r) ^+ m2 = paillier_enc (m1 *+ m2) (r ^+ m2)%g.

Encryption exponentiation distributes as scalar multiplication

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

No lemmas in the stats use this lemma.

Loading source code...