Verification of Security protocols (TU/e, course code: 2IMS15)

Canvas for materials and further information

Here we only give some basics. The course details and resources are provided on CANVAS.

Contact me if you are taking the course but not yet registered for it on CANVAS.

Course Basics

Accademic Year: 2017-2018

Who gives this course:

When: Quarter 3. (February till April 2018)

Time and Place: Wednesdays hours 5 and 6 (13:45-15:30) and Fridays hours 3 and 4 (10:45 - 12:30)

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.

image of time table


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