Formal Models and Techniques for Analyzing Security Protocols (Summer Term 2017)

5. July 2017 Next reading group: July 11
We will skip [Dreier et.al.] due to time constraints, and discuss [Blachet, Abadí, Fournet], Chapter 6 and Rati and Matthias' experiences with CryptoVerif and ProScript

29. June 2017 Next seminar: 04 Jul


11. May 2017 Hands-on session assignment.
The assignments for the hands-on session can be found on the literature list page. The start of the hands-on period will be announced here.

11. May 2017 Updated paper assignment.
The paper presentation assignment has been updated, please check the literature list.

2. May 2017 First reading group will take place *today* Tuesday, 2 p.m., in room 3.21 at CISPA, E9.1.
If you have missed the kick-off meeting, this is the last chance to participate! We will read the first chapter of the Tutorial, and learn

18. April 2017 Kick-Off meeting takes place on Mon, 24.04.2017, 16:15 in E 9.1, Room 0.06.
At this date, we will discuss proceedings and set the weekly slot for the seven sessions.

In this seminar, we will give a thorough and systematic introduction into the
current research on protocol verification. Security protocols are distributed
programs that use cryptography to securing communications. They govern our
daily lives, although we hardly notice. They are for instance used to secure
electronic payments, webpages and many services requiring authentication, e.g.,
facebook. There is a long history of design flaws in such protocols. As
protocol failure often has grave consequences, formal verification is
necessary. This is very challenging: security must hold in presence of an
arbitrary adversary, hence there is non-determinism not only in the order in
which messages arrive, but also in the messages itself.

This seminar follows the tutorial “Formal Models and Techniques for Analyzing
Security Protocols: A Tutorial” by Véronique Cortier and Steve Kremer, and
discusses each chapter in a weekly reading group. At each reading group, the
chapter is presented, discussed, and followed by the presentation and discussion
of one or two papers from current research that pertain to this chapter. The
aim is to provide an insight into cutting edge research while providing the
necessary foundation to understand and contextualize it.

1. Intro & running example
2. Messages and deduction
3. Equational theory and static equivalence
4. A cryptographic process calculus
5. Security properties
6. Automated verification: bounded case
7. Automated verification: unbounded case

The official registration for the seminar will occur at the kick-off meeting.
Students are encouraged to pre-register before this initial meeting by writing
an email to robert.kuennemann(aeht)cispa.saarland including name, matriculation number and field of study.

Pre-registration is not binding. For final registration you have to show up in
the kick-off meeting. Places for the final registration will be provided in the
order of pre-registration until all places are taken.

The main requirement of this course if active participation in the weekly
meeting. Each meeting will have the following structure:

1. Presentation of current chapter (by student).
2. Discussion of present chapter.
3. Presentation of first paper (by student).
4. Discussion of first paper.
5. Presentation of second paper (by student).
6. Discussion of second paper.

The assignment is prepared during the kick-off meeting. The presenations are
supposed to be light-weight and interactive, hence whiteboard-only. Everyone is
supposed to read and understand the current chapter. Everyone is supposed to
read the papers before the meeting and to have understood it
before or after the meeting.

Password-protected for copyright reasons. (Password will be given in kick-off lecture.)