[Verifpal] New Primitive: PKE_ENC/PKE_DEC

[Nadim Kobeissi]

Hello everyone,

I am happy to announce that Verifpal 0.8.7 introduces a new primitive:

	• PKE_ENC(G^key, plaintext): ciphertext. Public-key encryption.
	• PKE_DEC(key, PKE_ENC(G^key, plaintext)): plaintext. Public-key decryption.

This is basically useful to model RSA or ElGamal encryption. It’s worth noting that just like RSA and Elgamal, the resulting ciphertext is not authenticated.

An included model, `examples/pke_test.vp`, shows how to use this primitive. Also, the Verifpal User Manual has been updated to include documentation of this new primitive.

I am also planning to implement a Shamir Secret Sharing primitive soon.

By the way, I’m currently at Real World Crypto, feel free to say hello if you’re around! I have Verifpal stickers.

Nadim Kobeissi
Symbolic Software • https://symbolic.software