Formal Methods for Information Security (Summer Term 2014)

Lecturer: Prof. Dr.-Ing. Heiko Mantel and Jinwei Hu, Ph.D.
Format: Lecture with exercises (V4 + Ü2)
TUCAN Id: 20-00-0362-iv
Language: English
Place and time: Tuesday 11:40-13:20 in S2|02/C120
  Wednesday 9:50-11:30 in S1|03/226 (Exception: 07.05.2014 in S1|03/223)
  Thursday 9:50-11:30 in S2|02/C110
Midterm exam: Tuesday, 03.06.2014, 11:40-13:20 in room S101/A01
exam inspection: Thu, 03.07.2014, 15:00-16:00, S2|02 E302 (bring your student card and photo ID!)
Final exam: Thursday, 17.07.2014, 9:50-11:30 in room S103/221
New: The resulting grades can now be found in TUCaN.
Exam inspection: Tue, 09.09.2014, room S2|02 A213, at 13:00 (last names A-L) and 13:30 (last names M-Z)
Assistant: Dipl.-Inform. Richard Gay (office hour: Thu, 14:30-15:30)

News

  • The lecture will start on 15th April (Tuesday).

Online Materials

The internal page for participants can be accessed using the password that is communicated during the first lecture. The page contains the following slides and exercises, newest first:

  • Sample solutions for Exercise Sheet 12: v1.0
  • Exercise Sheet 12 (Information Theory and Information-Flow Security for Programs): v1.0
  • Sample solutions for Exercise Sheet 11: v1.0
  • Slides for Module 11 (Information-Flow Security for Programs): v1.0 (complete)
  • Exercise Sheet 11 (Possibilistic Information-Flow Security and MAKS): v1.0
  • Sample solutions for Exercise Sheet 10: v1.0
  • Slides for Module 10 (The Modular Assembly Kit for Security): v1.0
  • Sample solutions for Exercise Sheet 9: v1.1 v1.0
  • Exercise Sheet 9 (Intransitive Noninterference and Event Systems): v1.1 v1.0
  • Sample solutions for Exercise Sheet 8: v1.0
  • Slides for Module 9 (Information Flow Security for Composed Systems): v1.0 (complete)
  • Exercise Sheet 8 (Unwinding): v1.0
  • Sample solutions for Exercise Sheet 7: v1.0
  • Exercise Sheet 7 (Noninterference): v1.0
  • Sample solutions for Exercise Sheet 6: v1.0
  • Slides for Module 8 (Noninterference): v1.0 (complete)
  • Exercise Sheet 6 (The Take-Grant Model): v1.0
  • Slides for Module 7 (The Take-Grant Model and Graph-Based Specifications): v1.0
  • Sample solutions for Exercise Sheet 5: v1.1 v1.0
  • Exercise Sheet 5 (Multi-level Security and Bell/La Padula): v1.0
  • Slides for Module 6 (Access Control Models for Multi-Level Security): v1.0
  • Sample solutions for Exercise Sheet 4: v1.0
  • Exercise Sheet 4 (HRU Model and Safety): v1.0
  • Sample solutions for Exercise Sheet 3: v1.1
  • Script for Module 5 (Undecidability of Safety): v1.0
  • Exercise Sheet 3 (HRU Model): v1.1 v1.0
  • Sample solutions for Exercise Sheet 2: v1.1 v1.0
  • Slides for Module 4 (The HRU Model and Safety): v1.0
  • Sample solutions for Exercise Sheet 1: 1.2 v1.1 v1.0
  • Exercise Sheet 2 (Access Control and Logic): v1.0
  • Slides for Module 3 (Propositional Logic and Predicate Logic): v1.0
  • Exercise Sheet 1 (Modeling Authentication and Authorization): v1.0
  • Slides for Module 2 (Access Control: Modeling Authentication and Authorization): v1.0 of part 1, v1.0 of part 2
  • Slides for Module 1 (Making "Security" Precise): v1.0
  • Slides for Module 0 (Introduction): v1.1 v1.0

Content

The course (see also the description in TUCaN) gives an overview on formal approaches to:

  • formal modeling of security-critical systems
  • formal specification of security requirements
  • formal security analysis of systems
  • theoretical foundations for developing secure software by stepwise refinement and composition.

The topics covered include:

  • introduction to formal methods for information security
  • formal modeling and analysis of access control mechanisms
  • formal modeling and analysis of information flow control
  • formal modeling and analysis of security protocols
  • formal modeling of trust relationships in distributed systems

Prerequisites

Knowledge of Computer Science and Mathematics, equivalent to the first four Semesters in the Computer Science Bachelor program, in particular

  • ability to use formal languages and calculi
  • and basic knowledge about logic.

Literature

Scientific articles (to be announced in the lecture) and slides of the lectures (will be available online after the lecture). Additionally, e.g., one of the following books:

  • M. Bishop: "Computer Security", Addison-Wesley, 2002.
  • D. Gollmann: "Computer Security", Wiley, 2010.
  • C. P. Pfleeger, S. L. Pfleeger: "Security in Computing", Prentice Hall, 2006.
  • J. Viega, G. McGraw: "Building Secure Software", Addison-Wesley, 2011.
  • D. Denning: "Cryptography and Data Security", Addison Wesley, 1982 (out of print, but still available on the internet)

Last modified on 14 August 2014.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang