192.059 Formal Methods for Security and Privacy
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2023S, VU, 4.0h, 6.0EC


  • Semester hours: 4.0
  • Credits: 6.0
  • Type: VU Lecture and Exercise
  • Format: Presence

Learning outcomes

After successful completion of the course, students are able to develop a static analysis technique for enforcing security and privacy properties in a variety of domains, such as cryptographic protocols, programming languages, and bytecode.

In particular, this course explains the foundations of the static analysis of security and privacy properties, with a particular focus on type systems and SMT solving. Students will learn how to formalize a static analysis, how to prove its soundness, and how to implement it in an efficient way using state-of-the-art verification tools.  

Subject of course

  • Static Analysis of Cryptographic Protocols via type systems and SMT solving (F* and ProVerif)
  • Language-based Security (Non-Interference, Hyperproperties, and Side Channels)
  • Static Analysis of Bytecode (Ethereum Smart Contracts, F*, SMT - Solving)

Teaching methods

The course is based on a combination of lectures and two projects, which provide theoretical foundations as well as hands-on experience with state-of-the-art security verification tools (ProVerif, Z3, F*).


Mode of examination


Additional information

ECTS Breakdown:

25h lectures, tutorials, exam

35h self-study

90h projects and exercises

150 hours (6 ECTS)





Course dates

Tue10:00 - 12:0007.03.2023 - 27.06.2023FAV Hörsaal 2 Lecture
Tue08:00 - 12:0025.04.2023FAV Hörsaal 2 Lecture
Formal Methods for Security and Privacy - Single appointments
Tue07.03.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue14.03.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue21.03.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue28.03.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue18.04.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue25.04.202308:00 - 12:00FAV Hörsaal 2 Lecture
Tue25.04.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue02.05.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue09.05.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue16.05.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue23.05.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue06.06.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue13.06.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue20.06.202310:00 - 12:00FAV Hörsaal 2 Lecture
Tue27.06.202310:00 - 12:00FAV Hörsaal 2 Lecture

Examination modalities

Students will be evaluated based on a written exam and projects. 

Course registration

Begin End Deregistration end
13.02.2023 13:00 26.03.2023 14:00 26.03.2023 14:00



No lecture notes are available.

Previous knowledge

Some background in verification and security is ideal, but motivated students with a good background in either of them are also welcome to the course.