Formal Methods for Information Security (Summer Term 2016)

Lecturer:	Prof. Dr.-Ing. Heiko Mantel
Assistant:	Markus Tasch (Office Hour: Wednesdays, 17:00-18:00 in E322, please send an e-mail upfront)
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:	Wednesday, 01.06.2016, 09:50-11:30 (rooms: see below) IMPORTANT: Registration closes at May 1, 2016 Exam Inspection: The exam inspection takes place on Friday July 1, 2016 14:30-16:00 in S2|02 E302. (Do not forget to bring your student and personal id!)
Final exam:	Thursday, 14.07.2016, 11:40-13:20 (rooms: see below) Exam Inspection: The exam inspection takes place on Thursday October 6, 2016 16:00-17:30 in S2|02 E302. (Do not forget to bring your student and personal id!)
Max. participants:	80
Links:	TUCaN page (course id: 20-00-0362-iv) D120 Forum (bulletin board of the Fachschaft)

News

• Exam Inspection: The inspection for the final exam will be on Thu, 06.10.2016, at 16:00-17:30 in S2|02, E202. Bring your student ID card and official photo ID for authentication. The results should already be visible in TUCaN soon.
• Room Assignment Final Exam: The room for the final exam on Thu, 14.07.2015, 11:40-13:20, will be S1|01 A01 (in the basement of S1|01!). Bring your student ID card and official photo ID for authentication. Bring a blue or black pen (not pencil).
• Announcement (07.07.2016): On Wednesday 13.07.2016 the lecture slot  will be used for a questions and answers session before the exam. Please send us your questions via e-mail before Tuesday 12.07.2016 such that we can prepare and cluster the questions. Please send your e-mail to both Prof. Mantel and Markus Tasch.
• Exam Inspection Mid-Term Exam (23.06.2016): The exam inspection for the mid-term exam in Formal Methods for Information Security takes place on Friday July 1, 2016 14:30-16:00 in S2|02 E302. (Do not forget to bring your student and personal id!)
• Announcement (21.06.2016): The exercise session for exercise sheet 9 will happen on 22.06.2016 instead of 28.06.2016.
• Announcement (07.06.2016): Due to TU Meet & Move there will be no lecture or exercise on Wednesday 08.06.2016. The next lecture takes place on Thursday 09.06.2016 at the usual time.
• Room Assignment Mid-Term Exam: The room for the mid-term exam on Wed, 01.06.2015, 09:50-11:30, will be S1|01 A01 (in the basement of S1|01!). Bring your student ID card and official photo ID for authentication. Bring a blue or black pen (not pencil).
• Announcement (24.05.2016): On Tuesday 31.05.2016 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 to both Prof. Mantel and Markus Tasch.
• Announcement (12.05.2016): On Tuesday 17.05.2016 the proof on the undecidability of HRU saftey will be continued on the blackboard. The exercise session for exercise sheet 5 will happen on 18.05.2016 instead of 17.05.2016.
• Important (22.03.2016): The registration for the exam of the course Formal Methods in Information Security in TUCaN already starts at 01.04.2016 and closes at 01.05.2016! Make sure to register in time for the exam.
  

Online Materials

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

Content

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 21 September 2016.