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).