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.
- On September 25th, our main goal is to study non-interference properties with ProVerif. We will mostly use this set of slides.
- 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.