Modelling and Analysis of Security Protocols

Introduction

This is the website for the course "Modelling and Analysis of Security Protocols" taught by Tom Chothia in Leiden September to December 2007. Here you can find all the handouts, lecture slides, exercises and related papers and links for this course. You may also e-mail with course related questions at T.Chothia (a) cwi.nl

News:

The course is over, you may return to your lives.

If you are interested in doing a M.Sc. project based on anything to do with this course then e-mail me. A list of project ideas is available here.

The course feed back questionnaire is here. Please fill this out and return it to me, as your feed back can help me improve the course.

Course Description

Protocols describe how communication between computers takes place. While most protocols are simple enough to be written down in a few lines, designing correct protocols is notoriously hard. This course covers:
  • Examples of well-known protocols, including protocols for authentication and anonymous communication.
  • The good design of secure protocols, common kinds of attacks on protocols and how to stop these attacks.
  • Methods for verifying protocols such as formal logics, process calculi and model checking.
  • Tools that can be used to automate the formal analysis of protocols.
  • There are no formal requirements for this course, however good mathematical skills and an enjoyment of solving logic puzzles would be helpful.

    Year:  2007-2008
    Intended Group(s):  Master Computer Science
    Studypoints:  6
    Lecturer(s):  Dr. T. Chothia
    Examination:  The examination will be by presentations and practical assignments.


    Lectures
  • September 7th
  • Lecture 1: Introduction to Modelling Protocols
  • Lecture slides: powerpoint, pdf, 6up for printing.
  • The Handout for lecture 1.
  • All the information you need is in the handout, but if you are interested excellent further reading is:
  • "Protocols for Authentication and Key Establishment" by "Colin Boyd and Anish Mathuria", there are copies in the library, if there aren't enough for everyone who wants one please share.
  • Lecture 2: Cryptology for Protocol Analysis
  • Lecture slides: powerpoint, pdf, 6up for printing.
  • The Handout for lecture 2.
  • It is not necessary to understand the details of particular encryption schemes to be able to analysis protocol, but if you are interested details of AES can be found in this paper (pdf) and the details of RSA can be found on the "RSA Laboratories" website.

  • September 14th
  • Lecture 3: Protocol Goals
  • Lecture slides: powerpoint, pdf, 6up for printing.
  • Lecture 4: Attacks and Principles
  • Lecture slides: powerpoint, pdf, 6up for printing.
  • Both lectures use the same handout: Handout for lectures 3 and 4.
  • Recommended reading: Prudent Engineering Practice for Cryptographic Protocols by Martin Abadi and Roger Needham. Further information on the Diffe-Hellman protocol can be found in RFC 2631. By this point in the course you should have a basic understanding of security protocols therefore ...
  • September 14th Homework 1: You can get it here. It is due on the 28th of September. It will count as 1/6th of your total mark.

  • September 21st No Lecture

  • September 28th Lectures 5 and 6: The BAN logic framework.
    These lectures described the BAN logic frame framework for analysing protocols.
  • Lecture 5 slides: powerpoint, pdf, 6up for printing.
  • Lecture 6 didn't have powerpoint slides, instead BAN proofs were demonstrated using the JAPE tool and the paper A Logic of Authentication Burrows et al. was explained. You need the JAPE tool for homework 2 so please download and install it.
  • September 28th Homework 1 due.

  • October the 5th These lectures explained how to use the ProVerif tool to automatically verify security protocol.
  • Lecture 7: ProVerif1 Lecture slides: powerpoint, pdf, 6up for printing.
  • Lecture 8: ProVerif2 Lecture slides: powerpoint, pdf, 6up for printing.

  • October the 12th : Protocols for Anonymity
  • Lecture 9: Anonymity: Theory Lecture slides: powerpoint, pdf, 6up for printing.
  • Lecture 10: Anonymity: Practice Lecture slides: powerpoint, pdf, 6up for printing.
  • October 12th Homework 2: You can get it here. It is due on the 26th of October. It will count as 1/3th of your total mark.

  • October the 22th : Model Checking Probabilistic Protocols with PRISM
  • Lecture 11: Model Checking Lecture slides: powerpoint, pdf, 6up for printing.
  • Lecture 12: Probabilistic Model Checking For Anonymity Lecture slides: powerpoint, pdf, 6up for printing.
  • A large part of both Lectures was presented using the PRISM Model Checker the files used for the Lectures can be found here

  • October the 26th
  • Lecture 13: What You Can't Do With Protocols ... and How To Do It Anyway. Lecture slides: powerpoint, pdf, 6up for printing. This lecture covered the global consensus problem and how it can be solved using probability or a trusted third party.
  • Lecture 14: Real Life Security Protocols Lecture slides: powerpoint, pdf, 6up for printing.
  • The ssh demonstration is here, from this text you should be able to work out/guess that the protocol negotiates crypto-schemes, using Diffe-Hellman and then uses RSA to verify authenticity. We also discussed the IKEv2 protocol described in RFC 4306.
  • October the 26th : Homework 2 back.

  • November 2nd Student Presentation:
  • Wang Liang
  • Antanas KaziliĆ«nas: Simple Cross-Site Attack Prevention.
  • Renuka Autar A BitTorrent-Driven Distributed Denial-of-Service Attack.
  • Kristian Rietveld: A proposal for priority VoIP phone calls..

  • November 9th Student Presentation:
  • Chen Xiaojing: Simple Authentication for the Web.
  • Frank Takes: On BAN Logics for Industrial Security Protocols.
  • Gao Ruoyun: Finite-State Analysis of SSL.

  • November 16th Student Presentation:
  • Johan Groenen: Anonymity and Security in Delay Tolerant Networks.
  • Chao Xiaofei: Secure Crash Reporting in Vehicular Ad hoc Networks.
  • Joris Huizer: Hot or Not: Revealing Hidden Services by their Clock Skew.
  • Lennart Theil: Breaking EMAP.

  • November 23rd Student Presentation:
  • Bogumila Sobolewska: Security Analysis of Voice-over-IP Protocols.
  • Sjoerd van Egmond: A Survey of Bots Used for Distributed Denial of Service Attacks.
  • Stijn de Gouw: Probabilistic Model Checking of an Anonymity System.
  • Erik Gast: Agyaat: Providing Mutually Anonymous Services over Structured P2P Networks.

  • November 30rd Student Presentation:
  • Pieter Rogaar: Kerberos Version IV: Inductive Analysis of the Secrecy Goals.
  • Roy Kensmil : Towards Security Analyses of an Identity Federation Protocol for Web Services in Convergent Networks.
  • Erik Jongsma: Strand Spaces.
  • Alessandro Eccher The SRP Authentication and Key Exchange System.