EasyCrypt is a proof assistant used for verifying computational
security proofs of cryptographic constructions. It has been applied to
several prominent examples, including the SHA3 standard and a
critical component of AWS Key Management Services.

In this paper we enhance the EasyCrypt proof assistant to reason
about computational complexity of adversaries. The key technical
tool is a Hoare logic for reasoning about computational complexity
(execution time and oracle calls) of adversarial computations. Our
Hoare logic is built on top of the module system used by EasyCrypt
for modeling adversaries. We prove that our logic is sound w.r.t.
the semantics of EasyCrypt programs — we also provide
full semantics for the EasyCrypt module system, which was previously
lacking.

We showcase (for the first time in EasyCrypt and in other
computer-aided cryptographic tools) how our approach can express
precise relationships between the probability of adversarial success
and their execution time. In particular, we can quantify
existentially over adversaries in a complexity class, and express
general composition statements in simulation-based frameworks.
Moreover, such statements can be composed to derive standard
concrete security bounds for cryptographic constructions whose
security is proved in a modular way. As a main benefit of our
approach, we revisit security proofs of some well-known
cryptographic constructions and we present a new formalization of
Universal Composability (UC).

Go to Source of this post
Author Of this post:

By admin