Verification of Security protocols (TU/e)

Who gives this course:

• Sandro Etalle (responsible)
• Jerry den Hartog
• Mayla Bruso

Semester 2. Course code: 2IF02

Time: on Mondays hours 3 and 4 (10:45 - 12:30)

Place: Auditorium 14

NB: from 2011-2012, all students (so both Kerckhoff and non-Kerckhoff) follow 2IF02. The distinction between 2IF02 and 2IS35 has vanished starting this year. But: students who have followed the old 2IS35 course will still do the same 2IS35 exam.

OWinfo (2IF02). https://venus.tue.nl/owinfo-cgi/owi_0695.opl?vakcode=2IF02&studiejaar=2011

Instructions the assignment can be found here.

Course material and video lectures:

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

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

Program:

Block 3
1. (February 6) Introduction and Overview
2. (February 13) Formal Protocol Narrations: The Spi-calculus
3. (March 5) Secrecy and Secrecy Types (there are no classes on February 20 and 27)
4. (March 12) Secrecy Types for Asymmetric Cryptography. Authenticity and Authenticity Types.
5. (March 19) ProVerif: A Resolution Prover for Protocol Verification
6. (March 26) Secrecy and Authentication
7. (April 2) Information flow
Block 4
8. (April 23) Analysis of an E-voting Protocol in the Applied Pi Calculus
9. (May 7) Non-repudiation
10. (May 14) Exercises on ProVerif
11. (May 21) Anonmimity (1)
12. (June 4) Anonmimity (2) (There is no lecture on May 28th or 29th)
13. (June 11) Presentations (1)
14. (June 18) Presentations (2)

References

• C. Cremers. Scyther -- Semantics and Verification of Security Protocols, Introduction (Chapter 1). PhD thesis, TU Eindhoven, 2006.

• 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.

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

• 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.

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

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

• 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.

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

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

• M. Burrows, M. Abadi, R.M. Needham. A Logic of Authentication. In Proceedings of the Royal Society of London, 426, pp. 233-271, 1989.

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

• 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.

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

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

• 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.

• 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.

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

• 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.

• 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.

• 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.

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