Arvutiteaduse instituut
  1. Kursused
  2. 2014/15 kevad
  3. Verification of cryptography with EasyCrypt (MTAT.07.030)
EN
Logi sisse

Verification of cryptography with EasyCrypt 2014/15 kevad

  • Main
  • Installing Easycrypt

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 .ec files in the lecture folder).
  • Arvutiteaduse instituut
  • Loodus- ja täppisteaduste valdkond
  • Tartu Ülikool
Tehniliste probleemide või küsimuste korral kirjuta:

Kursuse sisu ja korralduslike küsimustega pöörduge kursuse korraldajate poole.
Õppematerjalide varalised autoriõigused kuuluvad Tartu Ülikoolile. Õppematerjalide kasutamine on lubatud autoriõiguse seaduses ettenähtud teose vaba kasutamise eesmärkidel ja tingimustel. Õppematerjalide kasutamisel on kasutaja kohustatud viitama õppematerjalide autorile.
Õppematerjalide kasutamine muudel eesmärkidel on lubatud ainult Tartu Ülikooli eelneval kirjalikul nõusolekul.
Tartu Ülikooli arvutiteaduse instituudi kursuste läbiviimist toetavad järgmised programmid:
euroopa sotsiaalfondi logo it akadeemia logo