CS882 - Security Protocols and Threat Models

TIMETABLE	TEACHING MATERIAL
Credits	20
Level	5
Semester	Semester 1
Availability
Prerequisites
Learning Activities Breakdown	Lectures: 10 x 2 hours. Laboratory: 11 x 2 hours (including revision lab in week 11). Private study: 158 hours.
Items of Assessment	2
Assessment	60% Exam, 40% Coursework. The coursework, consisting of exercises, will be formally assessed mid-term (20%) and at the end of the course (20%).
Lecturer	Ross Horne

Aims and Objectives

The aim of this course is to help students understand how vulnerabilities in systems can arise and be countered through the design and appropriate usage of protocols. Protocols are critical for almost all systems, which now typically involve multiple components, such as severs, clients, and other devices such as smartcards. The course is motivated via leading examples of protocols that fulfil different roles in such systems, and hence are intended to establish different security properties, such as mutual agreement and forward secrecy. Through case studies and pedagogical exercises, the students form an intuition for what the essential elements of security and privacy properties are, and for the underlying threat models that capture the capabilities of man-in-the-middle attackers which we aim to counter. This intuition facilitates students in the use of state-of-the-art tools for formally model and verify protocols. Students will then be able to use logical formulations of security properties in their tools chain for avoiding critical vulnerabilities in systems.

Learning Outcomes

At the end of this class, learners should be able:

To identify key features of security protocols and represent those features using message sequence charts and processes.
To understand how protocols are critical for a range of networked systems, including wired systems such as the Web, and wireless systems such as smartcards.
To precisely formulate security properties such as secrecy and authentication in various forms such as injective agreement, Mafia fraud, and forward secrecy.
To establish strong privacy properties of protocols, notably unlinkability and anonymity, and know how they relate to data minimisation.
To make use of tools and mental models to uncover vulnerabilities in protocols, ahead of attackers, and to evaluate the severity of vulnerabilities in different systems.

Syllabus

The course begins with simple examples illustrating common misconceptions when first encountering protocols. Famous examples, due to Dolev & Yao, help students understand that protocols must be resistant against attackers who may infiltrate and hence appear to be regular participants in the system. This will help students understand why simple-looking protocols are not easy to get right and why we need tools and methods to check them.

The course is driven by case studies. The case studies provide a strong security motivation and systems context, while at the same time illustrating progressively more challenging security and privacy problems, that the students understand through problems sheets that ensure they understand the key definitions and how to use tools to solve related problems. The course mainly uses the tool ProVerif.

RFID protocols. Electronic identity documents such as ePassports and other ID cards are increasingly used to authenticate users in setting critical for our society and economy. RFID cards have limited computational resources, and meaning they should achieve authentication with a simple design. The students study a series of protocols to understand what properties the security controls of Basic Access Control (BAC) and Password Authenticated Connection Establishment (PACE) protocols achieve. This helps the students form an intuition for various security and privacy properties that such protocols guarantee, including secrecy, injective agreement, and forward secrecy. We then consider the EMV protocol, that is used for ePayments, as a larger case-study where authentication properties are critical to avoid fraud.

Identity in authentication protocol design. We recall the famous story of the Needham-Schroeder protocol and use it to explain a threat model for public-key protocols. We then consider the message learnt in the context of larger modern protocols. We consider a ubiquitous single sign-on protocol, OpenID Connect (OIDC), which has become a standard way to authenticate online without spreading passwords over the internet. This requires the students to understand multi-party authentication and an understanding of HTTPS and PKI. However, we observe that the old lessons learnt from the Needham-Schoeder protocol still apply to these modern protocols.

Authentication using distance and time. We consider a form second-factor authentication, where a protocol can determine whether devices are in proximity, e.g., a car-key should be inside a car for ignition. We understand why these distance-bounding protocols are difficult to design, and the need to understand properties such as Mafia fraud. Student will the role of temporal properties, that can reason about the ordering of events, when specifying such properties. The exercises for this part of the course also consider the notion of recent aliveness, which considers whether something happened recently (which is not guaranteed by agreement for example). Formally, Mafia fraud and recent aliveness can be expressed using similar machinery, which student learn to define precisely and implement in tools.

The strong privacy property: unlinkability. The students examine the protocols studied already in the course with respect to privacy. We consider unlinkability problems in ePassport protocols and the EMV protocols, and approaches for addressing them. The students will understand how to model unlinkability as an equivalence problem between an ideal model where privacy holds by definition and a model of a real system where the user behaves as normal.

Office:	0141 548 3189/3096
	cis-office@strath.ac.uk
	LT1101
IT Support:	cis-support@strath.ac.uk
	0141 548 3592
	LT1307
Emergency:	0141 548 2222
Security Control:	0141 548 3333

Syllabuses - PG

CS882 - Security Protocols and Threat Models

Aims and Objectives

Learning Outcomes

Syllabus

Recommended Reading