BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Programming-Language Techniques for Secure Cryptography - Santiago
  Zanella Béguelin\, IMDEA
DTSTART:20110404T101500Z
DTEND:20110404T111500Z
UID:TALK30534@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Cryptographic primitives such as encryption and digital signat
 ure schemes form the building blocks of secure computer systems. Their sec
 urity 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 h
 istory of modern cryptography is fraught with examples of flawed security 
 proofs that stood unchallenged for years.\n\nA well established methodolog
 y 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 org
 anise 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.\n\nIn this talk I will show how game-base
 d proofs can be given formal foundations by representing games as probabil
 istic programs where adversaries are modelled as probabilistic polynomial-
 time procedures\, and relying on programming language techniques to justif
 y proof steps.\nThe techniques I will present have been implemented in the
  CertiCrypt framework\, itself built on top of the Coq proof assistant\, a
 nd include a probabilistic relational Hoare logic\, a theory of observatio
 nal equivalence\, and certified program transformations. CertiCrypt has be
 en 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.\n\nThe programming 
 language principles and techniques I developed to formalize game-based pro
 ofs transcend their initial application domain and allow to reason about p
 robabilistic programs in general. I will outline possible extensions (e.g.
  approximate equivalence)\, applications (e.g. quantitative information fl
 ow\, differential privacy) and opportunities for increasing automation.\n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR