EasyCrypt Reference Manual (PDF)
For your reading convenience, I have emended the hyperlinks in the introduction to point to online versions of the citations and not to the paper’s bibliography.
From the introduction:
EasyCrypt [BDG+14, BGHZ11] is a framework for interactively finding, constructing, and machine-checking security proofs of cryptographic constructions and protocols using the codebased sequence of games approach [BR04, BR06, Sho04]. In EasyCrypt, cryptographic games and algorithms are modeled as modules, which consist of procedures written in a simple userextensible imperative language featuring while loops and random sampling operations. Adversaries are modeled by abstract modules—modules whose code is not known and can be quantified over. Modules may be parameterized by abstract modules.
EasyCrypt has four logics: a probabilistic, relational Hoare logic (pRHL), relating pairs of procedures; a probabilistic Hoare logic (pHL) allowing one to carry out proofs about the probability of a procedure’s execution resulting in a postcondition holding; an ordinary (possibilistic) Hoare logic (HL); and an ambient higher-order logic for proving general mathematical facts and connecting judgments in the other logics. Once lemmas are expressed, proofs are carried out using tactics, logical rules embodying general reasoning principles, and which transform the current lemma (or goal) into zero or more subgoals—sufficient conditions for the original lemma to hold. Simple ambient logic goals may be automatically proved using SMT solvers. Proofs may be structured as sequences of lemmas, and EasyCrypt’s theories may be used to group together related types, predicates, operators, modules, axioms and lemmas. Theory parameters that may be left abstract when proving its lemmas—types, operators and predicates—may be instantiated via a cloning process, allowing the development of generic proofs that can later be instantiated with concrete parameters.
…
Be aware the documentation carries this warning (1.6 About this Documentation):
This document is intended as a reference manual for the EasyCrypt tool, and not as a tutorial on how to build a cryptographic proof, or how to conduct interactive proofs. We provide some detailed examples in Chapter 7, but they may still seem obscure even with a good understanding of cryptographic theory. We recommend experimenting.
My first time seeing documentation advising “experimenting” to understand it. 😉
You?
Before you jump to Chapter 7, be aware that Chapters 4 Structuring Specifications and Proofs, Chapter 5 EasyCrypt Library, Chapter 6 Advanced Features and Usage, and Chapter 7 Examples, have yet to be written.
You have time to work through the first three chapters and to experiment with EasyCrypt before being called upon to evaluate Chapter 7.
Enjoy!