Hash Proof Based Encryption Schemes in EasyCrypt
Master thesis
Permanent lenke
http://hdl.handle.net/11250/2560371Utgivelsesdato
2018Metadata
Vis full innførselSamlinger
Sammendrag
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.