Helper
benaloh_dec_correct
Signature
Lemma benaloh_dec_correct (m : 'Z_r) (u : {unit 'Z_n}) : benaloh_dec alpha (benaloh_enc m u) = Some m.
Description
Decryption with alpha recovers the original message
Uses (0)
This lemma does not use any other lemmas from the stats.
Used By (0)
No lemmas in the stats use this lemma.
Coq Source Code
View on GitHubLoading source code...