ElGamal decryption incorrect

Open MarkusKL opened this issue 10 months ago • 1 comments

It seems that the use of fst and snd are swapped in the ElGamal decryption algorithm in the examples. I would suggest adding a correctness game to AsymScheme.v and prove perfect correctness for the ElGamal scheme to make the correctness guarantee explicit.

I will attempt to make a PR with these changes in due time.

Feb 10 '25 15:02 MarkusKL

Encryption has shared secret as first component: https://github.com/SSProve/ssprove/blob/b5b89d660567d676b5c25533dae58dd397414593/theories/Crypt/examples/ElGamal.v#L159 Decryption computes inverse on the second component (not shared secret): https://github.com/SSProve/ssprove/blob/b5b89d660567d676b5c25533dae58dd397414593/theories/Crypt/examples/ElGamal.v#L166

Feb 10 '25 15:02 MarkusKL