Basic info
- Credits: 3 ECTS
- Time: Thursday 16:15-18:00, Friday 10:15-12:00 (in the period Feb 17 – March 14, 2025)
- Room: Delta, 2003
You will need to bring your own laptop.
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