18th Estonian Winter School in Computer Science (EWSCS)
XVIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 3 - 8, 2013

Santiago Zanella Béguelin

Microsoft Research, Cambridge
United Kingdom

Formal Methods for Cryptography


The security of cryptographic primitives like encryption and digital signature schemes is typically proven by reduction, showing that any feasible attack leads to an efficient solution to a hard problem. Yet these arguments are notoriously tricky and the history of modern cryptography is fraught with examples of flawed proofs that stood unchallenged for years. In this course I will present principles, techniques and tools to make writing and verifying proofs less prone to errors.

A common way to organize cryptographic proofs is to describe security as a game played between a challenger and an adversary, and to successively transform this initial experiment until reaching a game where it is clear that the adversary has little chance to win. The challenger sets up the game, answers to adversary queries, and determines whether the adversary succeeds. Such games can be described as probabilistic programs, turning the problem of verifying security into a program verification problem.

During this course I will show how to give formal foundations to game-based proofs using programming language techniques. Specifically, I will present a small probabilistic programming language to describe security experiments. I will describe the denotational semantics of this language and relational Hoare-style logics that can be used to prove approximate forms of program equivalence.

The techniques I will present are implemented in the EasyCrypt interactive theorem prover. An EasyCrypt proof consists of a sequence of games and relations between the probability of events in those games derived from relational Hoare-logic statements. I will demonstrate the usage of EasyCrypt to build security proofs of concrete primitives.

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed April 17, 2016 21:10 EET by local organizers, ewscs13(at)cs.ioc.ee
EWSCS'13 page: //cs.ioc.ee/ewscs/2013/