263-4600-00L  Formal Methods for Information Security

SemesterSpring Semester 2015
LecturersS. Radomirovic, M. Torabi Dashti
Periodicityyearly recurring course
Language of instructionEnglish

Catalogue data

AbstractThe course focuses on formal methods for the modelling and analysis of security and privacy concerns in critical systems, ranging from access control policies to cryptographic protocols.
ObjectiveThe students will learn the key ideas and theoretical foundations of formal modelling and analysis of security protocols and policies. The students will complement their theoretical knowledge by solving practical exercises and using various related tools.
ContentThe lecture treats formal methods for the modelling and analysis of security-critical systems.

The first part of the lecture focuses on access control policies in centralized and distributed settings. Access control policies are an integral part of modern Internet services; examples include single sign-on endpoints, distributed trust management in social Websites, and peer-to-peer networks. The lectures cover the formal foundations of authorization systems, and their applications to the synthesis and analysis of access control policies. We will also study a few notable existing models, such as XACML, DKAL and PBel.

The second part of the lecture concentrates on cryptographic protocols. Cryptographic protocols (such as SSL/TLS, SSH, Kerberos, SAML single-sign on, and IPSec) form the basis for secure communication and business processes. Numerous attacks on published protocols show that the design of cryptographic protocols is extremely error-prone. A rigorous analysis of these protocols is therefore indispensable. The lecture covers the theoretical basis for the formal modeling and analysis of such protocols. Specifically, we discuss their operational semantics, the formalization of security properties, and techniques and algorithms for their verification. In addition to the classical security properties for confidentiality and authentication, we will study privacy properties and the fairness property in contract signing. The accompanying tutorials provide an opportunity to apply the theory and tools to concrete protocols.

Performance assessment

Performance assessment information (valid until the course unit is held again)
Performance assessment as a semester course
ECTS credits4 credits
ExaminersM. Torabi Dashti, S. Radomirovic
Typesession examination
Language of examinationEnglish
RepetitionThe performance assessment is only offered in the session after the course unit. Repetition only possible after re-enrolling.
Mode of examinationoral 20 minutes
This information can be updated until the beginning of the semester; information on the examination timetable is binding.

Learning materials

Main linkFormal Methods for Information Security
Only public learning materials are listed.


263-4600-00 VFormal Methods for Information Security2 hrs
Thu09-11CAB G 57 »
S. Radomirovic, M. Torabi Dashti
263-4600-00 UFormal Methods for Information Security1 hrs
Thu11-12CAB G 57 »
S. Radomirovic, M. Torabi Dashti


No information on groups available.


There are no additional restrictions for the registration.

Offered in

Certificate of Advanced Studies in Computer ScienceFocus Courses and ElectivesWInformation
Computer Science MasterFocus Elective Courses Information SecurityWInformation