Symbolic Methods for Provable Security

Rigorous proofs are notoriously difficult to produce and verify even for seemingly simple cryptographic tasks. As a result, many published papers contain proofs that are most of the time incomplete and ocasionally flawed. Arguably, this indicates that the provable security paradigm is heading towards an undesirable crisis of rigor.

Significant research efforts are under way in order to correct this state of affairs. Examples, from the inside of the crypto community, include the works of Shoup, Bellare, and Rogaway on game playing techniques and Shai Halevi manifesto for machine assisted cryptographic proofs. Further inspiration comes from the outside of the crypto community. Symbolic methods and techniques commonly used in the areas of programming languages, language-based security, and logics have recently been employed to create general frameworks for computational security analysis.

The goal of this talk is to highlight the important role that symbolic methods could/should play within the general direction of provable security. I will present some of the existent results, exciting opportunities, and future challenges that stem from bringing together two research directions that for more than twenty years have developed largely indpendently.