The links below mostly do not work anymore. If you want the material from this lecture, please see here:
- Video recordings: http://www.uttv.ee/naita?id=21475
- Photos, homeworks, solutions: Attach:easycrypt-lecture-files.zip. (Files are suitable for a 2015 Easycrypt version and do not work with today's Easycrypt).
- Tejas Anil Shah updated part of the files from the lecture to a newer EasyCrypt version: Attach:easycrypt-lecture-files-updated-by-tejas-anil-shah.zip. (Tested with EasyCrypt git revisions ce56b105 and ea77e0ed from 2022.)
Basic info
- Credits: 3 ECTS
- Time: Mondays, 12:15-13:45
- Room: Room 003
Description
Cryptographic schemes (e.g., encryption schemes and such) are complex beasts, and the proofs of their security even more so. So it is no wonder that security proofs often have mistakes in them that stay undetected. So how can we trust them? One approach is to have a computer verify the security proofs.
In this lecture, we introduce the students to EasyCrypt (http://www.easycrypt.info). EasyCrypt is a tool for developing and verifying cryptographic proofs. Working with EasyCrypt, the student will understand:
- How cryptographic schemes are proven
- How computer aided theorem proving works (the workings of EasyCrypt are, in its basics, similar to those of many other tools such as Coq or Isabelle)
- How to formally reason about programs using Hoare logic
The lecture will consist of practical exercises with EasyCrypt. (And so will the homework and the exam.)
Materials
All the files used in the lecture can be found in the Windows share \\math.ut.ee\materjalid\easycrypt for used in the university network (also via eduroam). From outside, you can use the dropbox folder (https://www.dropbox.com/sh/jn35ty0y3sljql8/AADKa_iBT3H1rWajvgbYvWIIa?dl=0), but it may lag behind the Windows share.
- Video lectures: http://www.uttv.ee/naita?id=21475 (due to the video quality, they are best consumed with the photos and
.ecfiles in the lecture folder).