Verification of Security protocols (TU/e)

Course Basics

Accademic Year: 2016-2017

OWinfo (2IMS15).

Who gives this course:

When: Quarter 3. (February till April 2017) (Quarter calender)

Course code: 2IMS15 (replaces 2IF02)

Time and Place (see also OWinfo link above): Wednesdays hours 5 and 6 (13:45-15:30) in Flux 1.03 and Fridays hours 3 and 4 (10:45 - 12:30) in Flux 1.02 (amphi)


The assessment is performed through a written exam.

Exam date and time (see also OWinfo link above): Tuesday 11-04-2017 13:30-16:30 (register before 26-03-2017)
Resit (in Quartile 4): Thursday 29-06-2017 18:00-21:00 (register before 18-06-2017) room: Aud 14

Contact me if you still need to resit the old 2IF02 version of the course. (That version also includes an assignment.)

Course material and video lectures:

The most up to date version of the course material can be accessed directly at our svn repository here.

Below there are also reference to suggested reading.

In particular, the slides, which are updated during the course.

There are also handouts with supporting information such as a quick reference guide to SPI syntax handouts,

Another useful resource are the exercises that you can use to train and test your mastery of the material. You are expected to do this by self study; there are no supervised dedicated exercise sessions (with one possible exception see schedule below.) There is a short guide to help structure the available exercises and handouts. It also provides some additional exercises. There are some solutions available for you to check your answers. (Solve the exercises first, just looking at the solutions will not help.) If you still have questions you can ask the lecturers.

References to reading material are given below.

A few recordings of tele-lectures are available at (log in using your TU/e NT account, tue lectures, CS, 2IF02). Note, however, that this set is no where near complete.

Preliminary Schedule:

The following is the plan for topics treated in each lecture. There may be some changes during the course. Some suggested reading material related to the topic is also indicated. The references marked with * may contain parts that are beyond what is treated (up till then) in the course. The references [17]-[20] provide further background and examples. Note: schedule updated 14-2-2017
    Week Wednesday Friday
    1 Feb 8Introduction and Overview [1], [2, section 1-4], [5] Feb 10Formal Protocol Narrations: The Spi-calculus [handouts/spi.pdf],[15]*, [3]*
    2 Feb 15Secrecy [4, section 1-3] Feb 17ProVerif (1): A Resolution Prover for Protocol Verification [6],[7]
    3 Feb 22Authenticity[2, section 5] Feb 24Types for security [4, section 4-8],[6],[13]
    (No lectures Mar 1, 3 due to Carnaval)
    4 Mar 8ProVerif (2): Checking Authentication with ProVerif [2, section 7] Mar 10Strong Secrecy [16], [2, section 6]
    5 Mar 15 ProVerif (3): Analysis of an E-voting Protocol in the Applied Pi Calculus [14], [8] Mar 17 ProVerif (4): Non-repudiation, Fairness, Certified E-mail [10], [11], [12]
    6 Mar 22No lecture (!) Mar 24Anonymity (1): Strong anonymity, Dining Cryptographers[22], [9]
    7 Mar 29Anonymity (2): Probable Innocence, Crowds [23] Mar 31Anonymity (3): PRISM, probabilistic model checking [24], [25]
    8 April 5Catch up if needed otherwise question hours/Exam prep session. April 7(None planned)


    The links have been checked as of February 2017. (Some may only work from inside the campus/with VPN activated.) Let me know if any do not work.

    1. C. Cremers. Scyther -- Semantics and Verification of Security Protocols, Introduction (Chapter 1).

    2. M. Abadi. Security Protocols and Their Properties. . In NATO Science Series: Volume for the 20th International Summer School on Foundations of Secure Computation, pp. 39-60, Marktoberdorf, Germany, 1999.

    3. B. Pierce. Foundational Calculi for Programming Languages. In The Computer Science and Engineering Handbook, 1997.

    4. M. Abadi and B. Blanchet. Secrecy Types for Asymmetric Communication. In Conference on Foundations of Software Science and Computation Structures (FOSSACS), LNCS 2030, pp. 25-41, 2001.

    5. M. Abadi and R. Needham. Prudent Engineering Practice for Cryptographic Protocols. In IEEE Transactions on Software Engineering, 22(1):6-15, 1996.

    6. M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In Journal of the ACM, 52(1), pp. 102-146, 2005.

    7. B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW), pp. 82-96, 2001.

    8. L. C. Paulson. Inductive Analysis of the Internet Protocol TLS. In ACM Trans. on Information and System Security, 2(3), pp. 332-351, 1999.

    9. M. Burrows, M. Abadi, R.M. Needham. A Logic of Authentication. In Proceedings of the Royal Society of London, 426, pp. 233-271, 1989. (Technical Report version)

    10. J. Zhou, D. Gollmann A Fair Non-repudiation Protocol. In IEEE Symposium on Research on Security and Privacy, pp. 55-61, 1996.

    11. M. Abadi, N. Glew, B. Horne, B. Pinkas Certified E-mail with a Light On-line Trusted Third Party: Design and Implementation. In 11th Int. World Wid Web Conference, pp. 387-396, 2002.

    12. M. Abadi, B. Blanchet Computer-assisted Verification for Certified E-mail. In Science of Computer Programming, 58(1-2):3-27, 2005.

    13. M. Abadi. Secrecy by Typing in Security Protocols. In Journal of the ACM, 46(5), pp. 749-786, 1999.

    14. S. Kremer, M. Ryan. Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In 14th European Symposium on Programming (ESOP), pp. 186-200, 2005.

    15. M. Abadi, C. Fournet. Mobile Values, New Names, and Secure Communication. In 28th ACM Symposium on Principles of Programming Languages(POPL), pp. 104-115, 2001.

    16. B. Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In IEEE Symposium on Security and Privacy, pp. 86-100, 2004.

    17. B. Blanchet, M. Abadi, C. Fournet. Automated Verification of Selected Equivalences for Security Protocols. In 20th IEEE Symposium on Logic in Computer Science (LICS), pp. 331-340, 2005.

    18. M. Abadi, P. Rogaway. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In IFIP International Conference on Theoretical Computer Science (IFIP TCS), 2000.

    19. W. Aiello, S. Bellovin, M. Blaze, R. Canetti, J. Ioannidis, A. Keromytis, O. Reingold. Just Fast Keying: Key Agreement in a Hostile Internet. In ACM Transactions on Information and System Security, 7(2):242-273, 2004.

    20. M. Abadi, B. Blanchet, C. Fournet. Just Fast Keying in the Pi Calculus. In ACM Transactions on Information and System Security, 10(3), 2007.

    21. A. Gordon and A. Jeffrey. Authenticity Authenticity by Typing for Security Protocols. In Journal of Computer Security, 11(4), pp. 451-521, 2003.

    22. D. Chaum. The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability. In Journal of Cryptology 1(1), 1988, pp. 65-75.

    23. Sassone V, ElSalamouny E, Hamadou S. Trust in Crowds: probabilistic behaviour in anonymity protocols. In Trustworthly Global Computing 2010 Jan 1 (pp. 88-102). Springer Berlin Heidelberg.

    24. PRISM documentation

    25. Crowds PRISM case study

    Last modified: Feb 11 2016