Srdan Krstic: Catalogue data in Spring Semester 2022
|Name||Dr. Srdan Krstic|
Professur f. Informationssicherh.
ETH Zürich, CNB F 109.2
|Telephone||+41 44 632 93 28|
|252-0211-00L||Information Security||8 credits||4V + 3U||D. Hofheinz, S. Krstic, K. Paterson, J. L. Toro Pozo|
|Abstract||This course provides an introduction to Information Security. The focus|
is on fundamental concepts and models, basic cryptography, protocols and system security, and privacy and data protection. While the emphasis is on foundations, case studies will be given that examine different realizations of these ideas in practice.
|Objective||Master fundamental concepts in Information Security and their|
application to system building. (See objectives listed below for more details).
|Content||1. Introduction and Motivation (OBJECTIVE: Broad conceptual overview of information security) Motivation: implications of IT on society/economy, Classical security problems, Approaches to |
defining security and security goals, Abstractions, assumptions, and trust, Risk management and the human factor, Course verview. 2. Foundations of Cryptography (OBJECTIVE: Understand basic
cryptographic mechanisms and applications) Introduction, Basic concepts in cryptography: Overview, Types of Security, computational hardness, Abstraction of channel security properties, Symmetric
encryption, Hash functions, Message authentication codes, Public-key distribution, Public-key cryptosystems, Digital signatures, Application case studies, Comparison of encryption at different layers, VPN, SSL, Digital payment systems, blind signatures, e-cash, Time stamping 3. Key Management and Public-key Infrastructures (OBJECTIVE: Understand the basic mechanisms relevant in an Internet context) Key management in distributed systems, Exact characterization of requirements, the role of trust, Public-key Certificates, Public-key Infrastructures, Digital evidence and non-repudiation, Application case studies, Kerberos, X.509, PGP. 4. Security Protocols (OBJECTIVE: Understand network-oriented security, i.e.. how to employ building blocks to secure applications in (open) networks) Introduction, Requirements/properties, Establishing shared secrets, Principal and message origin authentication, Environmental assumptions, Dolev-Yao intruder model and
variants, Illustrative examples, Formal models and reasoning, Trace-based interleaving semantics, Inductive verification, or model-checking for falsification, Techniques for protocol design,
Application case study 1: from Needham-Schroeder Shared-Key to Kerberos, Application case study 2: from DH to IKE. 5. Access Control and Security Policies (OBJECTIVES: Study system-oriented security, i.e., policies, models, and mechanisms) Motivation (relationship to CIA, relationship to Crypto) and examples Concepts: policies versus models versus mechanisms, DAC and MAC, Modeling formalism, Access Control Matrix Model, Roll Based Access Control, Bell-LaPadula, Harrison-Ruzzo-Ullmann, Information flow, Chinese Wall, Biba, Clark-Wilson, System mechanisms: Operating Systems, Hardware Security Features, Reference Monitors, File-system protection, Application case studies 6. Anonymity and Privacy (OBJECTIVE: examine protection goals beyond standard CIA and corresponding mechanisms) Motivation and Definitions, Privacy, policies and policy languages, mechanisms, problems, Anonymity: simple mechanisms (pseudonyms, proxies), Application case studies: mix networks and crowds. 7. Larger application case study: GSM, mobility
|263-4600-00L||Formal Methods for Information Security||5 credits||2V + 1U + 1A||S. Krstic, R. Sasse, C. Sprenger|
|Abstract||The course focuses on formal methods for the modeling and analysis of security protocols for critical systems, ranging from authentication protocols for network security to electronic voting protocols and online banking. In addition, we will also introduce the notions of non-interference and runtime monitoring.|
|Objective||The students will learn the key ideas and theoretical foundations of formal modeling 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. The students also learn the fundamentals of non-interference and runtime monitoring.|
|Content||The course treats formal methods mainly for the modeling 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.|
The second part of this course will cover a selection of advanced topics in security protocols such as abstraction techniques for efficient verification, secure communication with humans, the link between symbolic protocol models and cryptographic models as well as RFID protocols (a staple of the Internet of Things) and electronic voting protocols, including the relevant privacy properties.
Moreover, we will give an introduction to two additional topics: non-interference as a general notion of secure systems, both from a semantic and a programming language perspective (type system), and runtime verification/monitoring to detect violations of security policies expressed as trace properties.