Mechanizing and Automating Cryptographic Arguments

Abstract

Cryptographic protocols are used to secure many applications. The goal of a cryptographic proof is to obtain formal guarantees on the level of security provided by such a protocol. Mechanization allows for the highest level of guarantees, by having a formal computer program verify the cryptographic arguments themselves. This approach has seen a growing interest in the last years, notably with the utilization of program logics to verify cryptographic games encoded as imperative programs (e.g. as in EasyCrypt).

The first goal of this talk is to present an alternative approach to mechanize cryptographic arguments. This approach, implemented in the Squirrel proof assistant, relies on a different encoding of cryptographic proofs: games are represented by pure instead of imperative programs, and cryptographic arguments are directly captured at a logical level. In particular, some of Squirrel logical rules corresponds to reductions to cryptographic hardness assumptions. Unfortunately, these rules are complex to design and implement; so far, these tasks are manual, error-prone, and limited to a small set of cryptographic assumptions (e.g. IND-CCA and PRF). The second goal of this talk is to present some recent work that aim at providing a formal, systematic and highly-automated method for deriving rules from cryptographic games. Our method relies on synthesizing (parts of) an adversary w.r.t. some cryptographic game through the notion of bi-deduction, and has been implemented in Squirrel.