BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Microsoft Research Cambridge\, public talks
SUMMARY:Programming-Language Techniques for Secure Cryptog
raphy - Santiago Zanella Béguelin\, IMDEA
DTSTART;TZID=Europe/London:20110404T111500
DTEND;TZID=Europe/London:20110404T121500
UID:TALK30534AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/30534
DESCRIPTION:Cryptographic primitives such as encryption and di
gital signature schemes form the building blocks o
f secure computer systems. Their security is usual
ly established by reduction\, showing that a feasi
ble attack would lead to an efficient way to solve
some computationally hard problem. Yet this kind
of arguments are notoriously difficult to verify a
nd the history of modern cryptography is fraught w
ith examples of flawed security proofs that stood
unchallenged for years.\n\nA well established meth
odology for structuring security proofs of cryptog
raphic primitives is to give a precise mathematica
l description of the interaction between an advers
ary and a challenger---such descriptions are refer
red to as games---and to organise proofs as sequen
ces of games\, starting from a game that represent
s a security goal and proceeding by successive tra
nsformations to games that represent security assu
mptions.\n\nIn this talk I will show how game-base
d proofs can be given formal foundations by repres
enting games as probabilistic programs where adver
saries are modelled as probabilistic polynomial-ti
me procedures\, and relying on programming languag
e techniques to justify proof steps.\nThe techniqu
es I will present have been implemented in the Cer
tiCrypt framework\, itself built on top of the Coq
proof assistant\, and include a probabilistic rel
ational Hoare logic\, a theory of observational eq
uivalence\, and certified program transformations.
CertiCrypt has been notably applied to obtain for
the first time machine-checked proofs of the secu
rity of the Optimal Asymmetric Encryption Scheme a
nd of an optimal bound on the security of Full-Dom
ain Hash signatures.\n\nThe programming language p
rinciples and techniques I developed to formalize
game-based proofs transcend their initial applicat
ion domain and allow to reason about probabilistic
programs in general. I will outline possible exte
nsions (e.g. approximate equivalence)\, applicatio
ns (e.g. quantitative information flow\, different
ial privacy) and opportunities for increasing auto
mation.\n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7
J J Thomson Avenue (Off Madingley Road)\, Cambrid
ge
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR