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

Exam date and time: July 5th 2013 14:00-17:00

NB: from 2011-2012, all students (so both Kerckhoff and non-Kerckhoff) follow 2IF02. The distinction between 2IF02 and 2IS35 has vanished starting that year.

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

Telelecturing and video lectures:

In Twente the telelecturing is in room CR3F

The connection problems with Nijmegen should be resolved.

Video lectures are available at http://videocollege.tue.nl (log in using your TU/e NT account and search for '2IF02' (tue lectures-(2)Computer science-2IF02)). For Block 3 the lecture numbers and content correspond to the schedule given below.

Course material:

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 4) Introduction and Overview.
2. (February 18) Formal Protocol Narrations: The Spi-calculus
3. (February 25) Secrecy and Secrecy Types
4. (March 4) Secrecy Types for Asymmetric Cryptography. Authenticity and Authenticity Types.
5. (March 11) Secrecy Types for Asymmetric Cryptography. Authenticity and Authenticity Types. (Continued)
6. (March 18) Information flow
7. (March 25) Anonymity (1)
Block 4
8. (April 22) Anonymity (2)
9. (May 6) Anonymity (3)
10. (May 13) ProVerif: A Resolution Prover for Protocol Verification
11. (May 27) Secrecy and Authentication
12. (June 3) Analysis of an E-voting Protocol in the Applied Pi Calculus
13. (June 10) Non-repudiation
14. (June 17) ProVerif Assignment.

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.