Krüptograafilised protokollid 2024/25 sügis

Lectures

The lecture slides will appear here sometime before (or perhaps after... hopefully before) the lecture.

• September 4th (plus some extra exercises for the first week).
• On September 11th, we will check out the ProVerif protocol analyser. Please have it installed on your computers. The lecture slides are here.
  • In the lecture, we played around with ProVerif. We considered our example program from the last week, and modelled its secrecy properties through a set of Horn clauses. The modelling went through a number of steps: 1, 2, 3, 4. We also considered a correspondence property and modelled it like this.
  • We tried to model the Yahalom protocol with Horn clauses, ending up with this model.
  • We saw our example protocol modelled in spi-calculus, first like this, and afterwards like this, where kept track, which party is honest.
• On September 18th, we continue with verifying trace properties in ProVerif. The material we cover is present in previous slide decks, but there is also some new material. We will see, how much we will manage to get through.
  • During the lecture, we created some ProVerif code: 1, 2, 3, 4.
• On September 25th, our main goal is to study non-interference properties with ProVerif. We will mostly use this set of slides.
  • During the lecture, we created some ProVerif code: 1, 2, 3, 4.
• On October 2nd, we'll speak about TLS, and start with Tamarin. We'll play around with these files - 1, 2, 3 - during the Tamarin part.
• On October 9th, we'll model some protocols in Tamarin from scratch. Please ensure that you can run Tamarin in your computer.
  • Protocol modeling is demonstrated using text editor gedit. Here is (inofficial) syntax highlighting of Tamarin (and also ProVerif) that can be used to make it more readable. In Linux, these files should be renamed from .txt to .lang and put into locations like .local/share/gtksourceview-4/language-specs or /usr/share/gtksourceview-4/language-specs (the precise location and the number X in gtksourceview-X may be different, just check where the .lang files for all the other languages are in your system). Tamarin manual refers to official syntax highlighting files for some other editors as well.
  • The Tamarin code of this session can be found in task1 and task2. Note that task2 requires to run Tamarin with --diff parameter to verify observational equivalence.
• On October 16th, we will end with Tamarin, doing some more tasks. We will also discuss how meaningful the symbolic model is.
  • The Tamarin code of this session can be found in task3 and task4.
• On October 23rd, we start with secure multiparty computation.
• On October 30th, we continue with passively secure multiparty computation, including extensions of oblivious transfers.
• On November 6th, we start with actively secure multiparty computation. We discuss definitions, including impossibility of broadcast protocol. We show a classical possibility result, and continue with the discussion of actively secure oblivious transfers (slides 9-11, 13, 14, 23-25) and actively secure MPC from secret sharing (slides 1-15). Perhaps we'll open this set of slides as well.