EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code.
EasyCrypt’s main application is the construction and verification of game-based cryptographic proofs. The objective of this security assessment was to identify and confirm potential security vulnerabilities.
IncludeSec identified 19 categories of findings. There were 2 deemed a “Critical-Risk,” 1 deemed a “High-Risk,” 3 deemed a “Medium-Risk,” and 10 deemed a “Low-Risk,” which pose some tangible security risk. Additionally, 3 “Informational” level findings were identified that do not immediately pose a security risk. The risks have since been addressed by EasyCrypt.
The full assessment and summary of findings can be found below.