Hash Proof Based Encryption Schemes in EasyCrypt

Abstract

We describe the basics of the proof-assistant \EasyCrypt{} and explain how to use \EasyCrypt{} to model encryption schemes and game-based security proofs. Furthermore, we analyze a generic encryption scheme by Cramer and Shoup, which is based on hash proof systems and the difficulty of deciding whether or not an element of a finite set $X$ lies in a certain subset $L \subset X$. We implement this scheme in \EasyCrypt{} and verify its security proof. We also present some simplifications of the scheme, making it easier to implement at the cost of less security. Finally, we concretize the simplified generic scheme using the Decision Diffie Hellman assumption.