Formal Methods for Information Security (Summer Term 2013)

Lecturer:	Prof. Dr.-Ing. Heiko Mantel
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
	Thursday 9:50-11:30 in S2|02/C110
Assistant:	Jinwei Hu, Ph.D.

Final exam inspection

The inspection will take place on Thursday, September 19 2013, 14:00 - 15:00 at S202 E302.

Please bring your student card and photo ID for the inspection.

Important Information for Final Exam

Date:	Thursday, July 18, 2013
Time:	9:50 - 11:40
Place:	S202/C205

Online materials in the internal page for participants

Solution 12 (Information Flow in Programs) v1.2

including remarks to the questions in class about the definitions of the confidential event set C for example properties

Module 12 (Summary) v1.0

Solution 11 (The Modular Assembly Kit for Security) v1.1

Solution 12 (Information Flow in Programs) v1.0

Solution 10 (Possibilistic Information Flow Security) v1.0

Exercise 10 (Possibilistic Information Flow Security) v1.1

Module 11 (Information Flow Security for Programs) v0.9

Module 11 (Information Flow Security for Programs) v1.0

Exercise 11 (The Modular Assembly Kit for Security) v1.0

Module 10 (The Modular Assembly Kit for Security) v1.0

Module 10 (The Modular Assembly Kit for Security) v1.0 Part 1 only!

Module 10 (The Modular Assembly Kit for Security) v0.9

Module 9 (Information Flow Security for Composed Systems) v1.0

Exercise 10 (Possibilistic Information Flow Security) v1.0

Module 9 (Information Flow Security for Composed Systems) Part 1, 2, and 3 v1.0

Solution 9 (Information Flow Security)

Solution 8 (Unwinding)

Exercise 9 (Information Flow Security)

Module 9 (Information Flow Security for Composed Systems) Part 1 and 2 v1.0

Module 9 (Information Flow Security for Composed Systems) v0.91

Module 9 (Information Flow Security for Composed Systems) v0.9

Module 9 (Information Flow Security for Composed Systems) Part 1 v1.0

Module 8 (Noninterference) v1.1

Exercise 8 (Unwinding) v1.0

Solution 7 (Noninterference) v1.0

Module 8 (Noninterference) part 1&2&3 v1.1

Module 8 (Noninterference) part 1&2 v1.0

Module 8 (Noninterference) v0.9

Exercise 7 (Noninterference) v1.0

Solution 6 (Take-Grant Model) v1.0

Exercise 6 (Take-Grant Model) v1.0

Module 7 (Take-Grant Model) v1.0

Module 7 (Take-Grant Model) v0.9

Solution 5 (MLS and BLP) v1.0

Solution 4 (Undecidability of safety) v1.0

Module 6 (Bell LaPadula Model) v1.0

Module 7 (Take-Grant Model) v1.0 part 1 and 2 only!

Exercise 5 (MLS and BLP) v1.0

Solution 3 (HRU) v1.0

Module 5 (Undecidability of safety) v1.0; see errata

Exercise 4 (Undecidability of safety) v1.1; see errata

Module 3 (HRU and safety) v1.1; see errata

Module 6 (Bell LaPadula Model) v0.9

Exercise 4 (Undecidability of safety) v1.0

Module 5 (Undecidability of safety) v0.9

Module 5 (Undecidability of safety) blackboard

Exercise 3 (HRU) v1.0

Solution 2 (Labeled Transition Systems and Access Control) v1.0

Slides for Module 4 (Propositional Logic and Predicate Logic) v1.0

Exercise 2 (Labeled Transition Systems and Access Control) v1.0

Solution 1 (Security Objectives and Access Control) v1.0

Exercise 1 (Security Objectives and Access Control) v1.1

Slides for Module 3 (HRU and Safety) v1.0 Part 1, 2, and 3

Slides for Module 2 (Access Control) v1.0, Module 3 (HRU and Safety) v1.0 Part1

Exercise 1 v1.0 (Security Objectives and Access Control)

Slides for Module 3 (HRU and Safety) v0.9

Slides for Module 2 (Access Control) v1.0 Part 1

Slides for Module 2 (Access Control) v0.9

Slides for Module 1 (Making Security Precise) v1.0

Slides for Module 0 (Introduction) v1.0

Midterm exam point announcement for individuals

Each participant may come to S202 E322 for the exam points during the following time slots.

Wednesday, June 26 2013, 15:00 - 16:00

Thursday, June 27 2013, 15:00 - 16:00

Please bring your student card and photo ID.

Midterm exam inspection

The inspection will take place on Friday, June 28 2013, 14:00 - 15:00 at S202 E302.

Please bring your student card and photo ID for the inspection.

News

Internal page for participants can be accessed using the password that is communicated during the first lecture.

The lecture will start on 17th April (Wednesday); no lecture on 16th April (Tuesday).

Important Information

Exam Registration Deadline:	May 5, 2013 (attention: Sunday!)
Mid-term Examination:	9:50 - 11:40 Wednesday, June 5, 2013 at S1|03/226
Final Examination:	Thursday, July 18, 2013

Content

The course (see also the description of the module) 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", Pearson Education, 2002.
• D. Gollmann: "Computer Security", Wiley, 2010.
• C. P. Pfleeger, S. L. Pfleeger: "Security in Computing", Pearson Education, 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 26 March 2014.