Helper

decryption_unique

Section paillier_params

Type Lemma

Proof Lines 4

Lemma decryption_unique (m1 m2 : 'Z_n) (r1 r2 : {unit 'Z_n2}) : (paillier_enc m1 r1) ^+ lambda = (paillier_enc m2 r2) ^+ lambda -> m1 = m2.

Distinct messages give distinct lambda-powers (unique decryption)

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

No lemmas in the stats use this lemma.

Loading source code...