Programming-Language Techniques for Secure Cryptography

Add to your list(s) Download to your calendar using vCal

• Santiago Zanella Béguelin, IMDEA
• Monday 04 April 2011, 11:15-12:15
• Large lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Cryptographic primitives such as encryption and digital signature schemes form the building blocks of secure computer systems. Their security is usually established by reduction, showing that a feasible attack would lead to an efficient way to solve some computationally hard problem. Yet this kind of arguments are notoriously difficult to verify and the history of modern cryptography is fraught with examples of flawed security proofs that stood unchallenged for years.

A well established methodology for structuring security proofs of cryptographic primitives is to give a precise mathematical description of the interaction between an adversary and a challenger—-such descriptions are referred to as games—-and to organise proofs as sequences of games, starting from a game that represents a security goal and proceeding by successive transformations to games that represent security assumptions.

In this talk I will show how game-based proofs can be given formal foundations by representing games as probabilistic programs where adversaries are modelled as probabilistic polynomial-time procedures, and relying on programming language techniques to justify proof steps. The techniques I will present have been implemented in the CertiCrypt framework, itself built on top of the Coq proof assistant, and include a probabilistic relational Hoare logic, a theory of observational equivalence, and certified program transformations. CertiCrypt has been notably applied to obtain for the first time machine-checked proofs of the security of the Optimal Asymmetric Encryption Scheme and of an optimal bound on the security of Full-Domain Hash signatures.

The programming language principles and techniques I developed to formalize game-based proofs transcend their initial application domain and allow to reason about probabilistic programs in general. I will outline possible extensions (e.g. approximate equivalence), applications (e.g. quantitative information flow, differential privacy) and opportunities for increasing automation.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Large lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.