Formal Methods for Information Security (Summer Term 2017)

Lecturer:	Prof. Dr.-Ing. Heiko Mantel
Assistants:	Markus Tasch (Office Hour: see page of the assistant) Ximeng Li, Ph.D.
Format:	Integrated course (IV6)
Language:	English
Place and time:	Tuesday 11:40-13:20 in S2|02/C110
	Wednesday 9:50-11:30 in S2|02/C110
	Thursday 9:50-11:30 in S2|02/C110
Midterm exam:	Tuesday, June 6, 11:40 – 13:20
Final exam:	Thursday, July 20, 09:50 – 11:30 in S2|02/C110!
Max. participants:	80
Links:	TUCaN page (course id: 20-00-0362-iv) D120 Forum (bulletin board of the Fachschaft)

News

• Final-Term Exam Inspection on Thursday 26.10.2017: The exam inspection for the final-term exam will take place on Thursday  26.10.2017, 16:00-16:45 in A313. Bring your student ID card and official photo ID for authentication.
• Room Final Exam on Thursday 20.07.2017: The room for the final exam on Thursday, 20.07.2017, 09:50-11:30, will be S2|02 C110 (i.e. the usual room for the lecture). Bring your student ID card and official photo ID for authentication. Bring a blue or black pen (not pencil).
• Announcement (13.07.2017): On Wednesday 19.07.2017 a part of the lecture will be used for a questions and answers session before the exam. Please send us your questions via e-mail in advance such that we can prepare and cluster the questions. Please send your e-mail with questions to Markus Tasch with CC to Prof. Mantel and Ximeng Li until Tuesday 16:00.
• Announcement (04.07.2017): There will be a lecture on 05.07.2017 instead of the exercise session for Exercise 11. The exercise session for Exercise 11 will instead take place on Thursday 06.07.2017.
• Mid-Term Exam Inspection on Thursday 29.06.2017: The exam inspection for the mid-term exam will take place on Thursday 29.06.2017, 16:00-17:00 in A126. Bring your student ID card and official photo ID for authentication.
• Room Mid-Term Exam on Tuesday 06.06.2017: The room for the mid-term exam on Tuesday, 06.06.2017, 11:40-13:20, will be S1|05 122 (Maschinenhaus). Bring your student ID card and official photo ID for authentication. Bring a blue or black pen (not pencil).
• Announcement (30.05.2017): On Thursday 01.06.2017 a part of the lecture will be used for a questions and answers session before the exam. Please send us your questions via e-mail in advance such that we can prepare and cluster the questions. Please send your e-mail with questions to Markus Tasch with CC to Prof. Mantel until Wednesday 05:30pm.

Online Materials

The online material can be accessed here using the password communicated in the first lecture.

Content

When talking about security of IT systems, best-practices for the development of secure systems or mechanisms for the protection of systems against illegal access of valuable assets play a major role. With this focus systems are called "secure" when the security appears substantiated by the used design processes and the deployed security mechanisms. This focus does not allow an objective assessment of the security properties the IT system does actually satisfy. To enable such an assessment, it is a necessity to make the desired security properties explicit with the necessary level of precision, to provide a view on the system appropriate to analyze the security of a system wrt. the desired requirements and to come up with analysis techniques to ease the process of judging the security of a system.

The course 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

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, 2015.
• 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)
  

Reference literature on logics and automata theory

• H.-D. Ebbinghaus, J. Flum, and W. Thomas: "Mathematical Logic", 2nd Edition, Springer, 1996.
• H.-D. Ebbinghaus, J. Flum, and W. Thomas: "Einführung in die mathematische Logik", 5th edition, Spektrum, 2007.
• J. E. Hopcroft, R. Motwani, and J. Ullman: "Introduction To Automata Theory, Languages, And Computation", Pearson Education Limited, 2013.

Last modified on 19 March 2018.