Modulcode:	infESSS-02a
Englische Bezeichnung:	Engineering Secure Software Systems
Modulverantwortliche(r):	PD Dr. Henning Schnoor
Turnus:	jedes Jahr im WS (WS22/23 WS23/24 WS24/25 WS25/26)
Präsenzzeiten:	3V 1Ü
ECTS:	6
Workload:	45 h lectures, 15 h exercises, 105 h self studies
Dauer:	ein Semester
Modulkategorien:	BSc-Inf-WP (BSc Inf (21)) WI (BSc Inf (15)) WI (BSc Inf) MSc-Inf-Theo (MSc Inf (21)) MSc-Inf-WP (MSc Inf (21)) 2F-MEd-Inf-WP (MEd-Hdl Inf (21)) 2F-MA-Inf-WP (2F-MA Inf (21)) MSc-WInf-WP-Inf (MSc WInf (21)) TI (MSc Inf (15)) WI (MSc Inf (15)) WI (MSc WInf (15)) WI (MSc WInf) IG (MSc Inf) TG (MSc Inf)
Lehrsprache:	Englisch
Voraussetzungen:

Kurzfassung:

The topic of this cource is the security of software systems. Key topics are specification and analysis of security properties as well as the design of secure systems (with regard to a given specification). The main examples of softwate systems studied in the course are cryptographic protocols and general state-based systems (in the sense of information flow analysis).

Lernziele:

The students learn basic properties of cryptographic protocols and prominent examples (e.g., authentication and key exchange) and know the fundamental techniques of information flow analysis. They can specify security properties of protocols and information-flow based systems formally and analyze a given system (both manually and with tool assistance) for security flaws. In addition they are familiar with design principles that guarantee specific security properties.

Lehrinhalte:

• examples for cryptographic protocols and attacks on protocols
• adversary capabilities and security goals
• information-flow properties
• manual and tool-assisted analysis of protocols and systems with respect to reachability properties
• formal analysis techniques for epistemic (knowledge-based) security properties of protocols

Weitere Voraussetzungen:

• Datenstrukturen und Algorithmen
• Theoretische Grundlagen der Informatik
• Berechnungen und Logik oder Logik in der Informatik

Prüfungsleistung:

oral exam

Lehr- und Lernmethoden:

Interactive lecture, exercise classes with examples, additional proofs and tool applications.

Verwendbarkeit:

Literatur:

• Michaël Rusinowitch and Mathieu Turuani. Protocol insecurity with a finite number of sessions, composed keys is NP-complete. In: Theoretical Computer Science 1-3.299 (2003), pp. 451-475
• Vincent Cheval, Véronique Cortier, and Mathieu Turuani. A Little More Conversation, a Little Less Action, a Lot More Satisfaction: Global States in ProVerif. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018. IEEE Computer Society, 2018, pp. 344-358. isbn: 978-1-5386-6680-7. doi: 0.1109/CSF.2018.00032. url: https://doi.org/10.1109/CSF.2018.00032
• Martin Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories. In: Theoretical Computer Science 367.1-2 (2006), pp. 2-32
• Ron van der Meyden. What, Indeed, Is Intransitive Noninterference? In: European Symposium On Research In Computer Security (ESORICS). ed. by Joachim Biskup and Javier Lopez. Vol. 4734. Lecture Notes in Computer Science. Springer, 2007, pp. 235-250. isbn: 978-3-540-74834-2
• Véronique Cortier, Stéphanie Delaune, and Vaishnavi Sundararajan. A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties. In: J. Autom. Reason. 65.4 (2021), pp. 479-520. doi: 10.1007/s10817- 020- 09582- 9. url: https://doi.org/10.1007/s10817-020-09582-9

Verweise:

Kommentar: