Christoph Sprenger: Catalogue data in Spring Semester 2019
|Name||Dr. Christoph Sprenger|
Institut f. Informationssicherheit
ETH Zürich, CNB F 108
|Telephone||+41 44 632 75 56|
|263-4600-00L||Formal Methods for Information Security||4 credits||2V + 1U||R. Sasse, C. Sprenger|
|Abstract||The course focuses on formal methods for the modelling and analysis of security protocols for critical systems, ranging from authentication protocols for network security to electronic voting protocols and online banking.|
|Objective||The students will learn the key ideas and theoretical foundations of formal modelling and analysis of security protocols. The students will complement their theoretical knowledge by solving practical exercises, completing a small project, and using state-of-the-art tools.|
|Content||The course treats formal methods mainly for the modelling and analysis of security protocols. Cryptographic protocols (such as SSL/TLS, SSH, Kerberos, SAML single-sign on, and IPSec) form the basis for secure communication and business processes. Numerous attacks on published protocols show that the design of cryptographic protocols is extremely error-prone. A rigorous analysis of these protocols is therefore indispensable, and manual analysis is insufficient. The lectures cover the theoretical basis for the (tool-supported) formal modeling and analysis of such protocols. Specifically, we discuss their operational semantics, the formalization of security properties, and techniques and algorithms for their verification.|
In addition to the classical security properties for confidentiality and authentication, we will study strong secrecy and privacy properties. We will discuss electronic voting protocols, and RFID protocols (a staple of the Internet of Things), where these properties are central. The accompanying tutorials provide an opportunity to apply the theory and tools to concrete protocols. Moreover, we will discuss methods to abstract and refine security protocols and the link between symbolic protocol models and cryptographic models.
Furthermore, we will also present a security notion for general systems based on non-interference as well as language-based information flow security where non-interference is enforced via a type system.
|263-4630-00L||Computer-Aided Modelling and Reasoning |
In the Master Programme max. 10 credits can be accounted by Labs on top of the Interfocus Courses. Additional Labs will be listed on the Addendum.
|8 credits||7P||C. Sprenger, D. Traytel|
|Abstract||The "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The lab has two parts: The first introduces various modelling and proof techniques. The second part consists of a project in which the students apply these techniques|
|Objective||The students learn to effectively use a theorem prover to create unambiguous models and rigorously analyse them. They learn how to write precise and concise specifications, to exploit the theorem prover as a tool for checking and analysing such models and for taming their complexity, and to extract certified executable implementations from such specifications.|
|Content||The "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The focus is on applying logical methods to concrete problems supported by a theorem prover. The course will demonstrate the challenges of formal rigor, but also the benefits of machine support in modelling, proving and validating.|
The lab will have two parts: The first part introduces basic and advanced modelling techniques (functional programs, inductive definitions, modules), the associated proof techniques (term rewriting, resolution, induction, proof automation), and compilation of the models to certified executable code. In the second part, the students work in teams of two on a project assignment in which they apply these techniques: they build a formal model and prove its desired properties. The project lies in the area of programming languages, model checking, or information security.
|Literature||Textbook: Tobias Nipkow, Gerwin Klein. Concrete Semantics, part 1 (www.concrete-semantics.org)|