Modelling and analysis of security protocols, 6 credits

Security protocols are special programs that protect us against the security threats posed by "adversaries" present on a communication network. For example, a security protocol might ensure that credit card details submitted to a web store remain confidential, or ensure that downloaded software originates from the sourse from which it purports to originate, or ensure that messages cannot be tracked back to their sender.

Though security protocols are small and simple-looking, they very often contain unexpected flaws: It is extreemely difficult to foresee all the possible ways in which the adversary may act in order to subvert the protocol. Over the past decades, therefore, a number of mathematical techniques have been developed for analyzing the properties of security protocols.

In this course, we focus on a particular approach for security protocol analysis. Roughly, the approach is as follows:

1. The protocol and its intended goals, such as secrecy, authentication, anonymity, etc, are described formally in CSP, an abstract programming language.

2. The abstract description is fed to the model checker FDR, which tests whether the protocol correctly achieves its goals. In the case where the system does not meet a goal, the model checker returns the sequence of steps the adversary must take in order to subvert the protocol.

Course goal

Upon completion of the course, the student will be able to describe a security protocol and its desired properties in a precise mathematical way, and use the tools and methods covered in the course to perform a security analysis.

Course content

1. The nature and role of security protocols and their vulnerabilities.

2. A mathematical framework for defining security protocols and their goals: An introduction to CSP, Modelling security protocols in CSP, Expressing protocol goals in CSP

3. Tools and techniques used to design and evaluate security protocols: The FDR model checker, The Casper compiler, Simplifying transformations

Prerequisites

There are no formal requirements for this course. However good mathematical skills and familiarity with automata theory would be helpful.

Examination

The examination for the course consists of homework assignments and a mini project. For the project, students select a (simple) security protocol to analyze, describe the protocol and its desired properties in a precise way, and use the tools and methods covered in the course to perform a security analysis.