EasyCrypt

EasyCrypt is an interactive framework for verifying the security of cryptographic constructions in the computational model. EasyCrypt adopts the codebased approach, in which security goals and hardness assumptions are modelled as probabilistic programs (called experiments or games) with unspecified adversarial code, and uses tools issued from program verification and programming language theory to rigorously justify cryptographic reasoning.

EasyCrypt is part of the Formosa project.

Resources

• Find us on GitHub
• Installing EasyCrypt
• Check out our new tutorial
• We have a reference manual. However, note that this reference manual has not been updated for years now and does not reflect the current (stable & unstable) status of EasyCrypt.
• We are currently revamping our documentation on program logic tactics.