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

Santiago Zanella Béguelin

Microsoft Research, Cambridge
United Kingdom

Formal Methods for Cryptography

Abstract

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

• S. Zanella Béguelin. Formal methods for cryptography. EWSCS 2013 course slides. Lecture 1 [pdf], lecture 2 [pdf], lecture 3 [pdf], lecture 4 [pdf].
• Videos from the lectures.
  • Lecture 1 [mp4]
  • Lecture 2 [mp4]
  • Lecture 3 [mp4]
  • Lecture 4 [mp4]
• M. Bellare and P. Rogaway. Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Report 2004/331. [link]
• S. Halevi. A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181. [link]
• S. Zanella-Béguelin. Formal certification of game-based cryptographic proofs. PhD thesis, Ecole Nationale Supérieure des Mines de Paris, 2010. [pdf]
• G. Barthe, B. Grégoire, S. Heraud, S. Zanella-Béguelin. Computer-aided security proofs for the working cryptographer. In P. Rogaway, ed., Proc. of 31th Ann. Int. Cryptology Conf., CRYPTO 2011, v. 6841 of Lect. Notes in Comput. Sci., pp. 71-90. Springer, 2011. [doi link]
• G. Barthe, J. M. Crespo, B. Grégoire, C. Kunz, S. Zanella-Béguelin. Computer-aided cryptographic proofs. In L. Beringer, A. Felty, eds., Proc. of 3rd Int. Conf. on Interactive Theorem Proving, ITP 2012, v. 7406 of Lect. Notes in Comput. Sci., pp. 11-27. Springer 2012. [doi link]
• G. Barthe, B. Grégoire, S. Zanella-Béguelin. Formal certification of code-based cryptographic proofs. J. of ACM, submitted.

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