Cryptographic Protocols

Link for the Coursework:

Literature:

1. Protocols for Authentication and Key Establishment.
   C. Boyd, A. Mathuria. Springer-Verlag. 2003.
2. Slides of Tutorial AVASP'05 (Automated Validation of Security Protocols)
   by Sebastian Mödersheim, Luca Viganò, David von Oheimb
3. Cryptography and Network Security.
   W. Stallings. Pearson Education, Prentice Hall. 2003.

• SPORE Security Protocols Open Repository
• The AVISPA Project

Lecture Log and Complementary Literature:

1. Lecture 1: Introduction and Motivation


2. Lecture 2: Basic Concepts of Cryptography and Applications
   • Encryption schemes
   • Kerckhoff's Principle
   • Security of encryption schemes
   • Symmetric cryptography
   • Public-key cryptography
   • Digital signatures
   • Cryptographic hash functions
   • Message authentication codes
   
   
3. Literature to Lectures 1 and 2:
   • More on cryptography itself:
     Cryptography: Theory and Practice (2nd Edition).
     D. R. Stinson. Chapman & Hall/CRC. 2002.
   • More on security of encryption schemes:
     Foundations of Cryptography, Vol. 1 & 2.
     O. Goldreich. Cambridge University Press. 2001/2004.
     Preliminary drafts available online.
   • Textbook chapters which provide an overview:
     • Computer Networks (4th edition), Chapter 8: Network Security.
       A. Tanenbaum. Pearson Education, Prentice Hall. 2003.
     • Distributed Systems: Concepts and Design (3rd edition), Chapter 7: Security.
       G. Coulouris, J. Dollimore, T. Kindberg. Pearson Education, Addison Wesley. 2001.
     • Communication and Networks: Fundamental Concepts and Key Architectures (2nd edition),
       Chapter 11: Security Protocols. A. Leon-Garcia, I. Widjaja. McGraw-Hill. 2004.
   
   
4. Lecture 3: Protocols and Attacks I
   • Notational conventions
   • Efficiency, computational and communications
   • Cryptanalysis vulnerability
   • Correctness
     • Assumptions: perfect cryptography, Dolev-Yao Intruder model
     • Protocol goals: extensional versus intensional goals,
       matching-conversations goal, always possible and not considered a real attack: relay attacks
   • Protocols for authentication
   • Basic symmetric key/public-key one-way authentication
   • Mutual challenge response protocols and attacks against them
   • Examples of correct mutual authentication
   
   
5. Lecture 4: Protocols and Attacks II
   • Protocols for authentication, continued
     • Goals for authentication
     • Needham-Schroeder Public Key
   • Protocols for key establishment
   • Classification in key transport, key agreement, hybrid
   • Goals for key establishment
   • Wide-Mouthed-Frog
   • Needham-Schroeder Symmetric Key
   • Simplified Kerberos Protocol
   • Abadi and Needham's principles for prudent engineering of security protocols


6. Lecture 5: Protocols and Attacks III
   
   • Protocols for key transport, continued
     • Otway-Rees, type-flaw attack
   • Protocols for key agreement
     • Diffie-Hellman Key Exchange
     • STS Protocol


7. Literature to Lectures 3 to 5:
   • [1] Sections 2.1-2.3, 3.2, 3.4, 4.2, 4.3, 5.2, 5.5.1; Chapter 1 gives a good overall introduction.
   • [2] Module 1: Introduction to security protocols
   • Systematic design of a family of attack-resistant authentication protocols.
     R. Bird, I. Gopal, A. Herzberg, P. Janson, S. Kutten, R. Molva, M. Yung.
     IEEE Journal on Selected Areas in Communications, 11(5):679-693, 1993
   • Prudent engineering practice for cryptographic protocols.
     M. Abadi, R. Needham. IEEE Symposium on Research in Security and Privacy. 1994.


8. Lecture 6: Real Life Protocols I: Kerberos


9.     Literature and Links:
   • Kerberos: The Definitive Guide. J. Garman. O'Reilly. 2003.
   • [3] Section 14.1
   • Kerberos: An Authentication Service for Computer Networks.
     B.C. Neuman, T. Ts'o. IEE Communications Magazine, 32(9):33-38. 1994.
   • Kerberos home page.


10. Lecture 7: Real Life Protocols II: SSL and TLS


11.     Literature and Links:
    • [3] Section 17.2
    • SSL 3.0 Specification.
    • The IETF TLS Workgroup.
    • The TLS Protocol, Version 1.0.


12. Lecture 8: Formal Models I: The Strand Space Model


13. Lecture 9: Applying the Strand Space Model
    
    • Proving the Needham-Schroeder-Lowe Protocol correct.


14. Literature and Links to Lectures 8 and 9:
    • Strand Spaces: Why is a Security Protocol Correct?
      F. J. Thayer Fabrega, J. C. Herzog, J. D. Guttman.
      IEEE Symposium on Security and Privacy, 1998.
    • The Strand Space Method home page.


15. Lecture 10: Discourse into Universal Algebra: Free Algebras


16. Lecture 11: Formal Models II: The Multiset Rewriting Model


17. Lecture 12: (Un)decidability and Complexity of Security Problems I
    • Proof of undecidability of MSR Secrecy.


18. Lecture 13: (Un)decidability and Complexity of Security Problems II
    • Overview of positive results.
    • Proof of DEXP-completeness of MSR Secrecy with bounded nonces and message size.


19. Literature to Lectures 11 to 13:
    • Multiset Rewriting and the Complexity of Bounded Security Protocols.
      N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov.
      Journal of Computer Security 12(2004):247-311.
      
    • [2] Module 3: Formal Methods for Security Protocols, pages 42 - 52.
    
    
20. Lecture 14:
    • Quick Overview of General Methodology and Tools
    • Logic for Beliefs: BAN Logic


21.     Literature:
    • [2] Module 3: Formal Methods for Security Protocols.
      Slides on BAN logic: pages 54 - 69.
      Slides on the AVISPA Tool: pages 98 - 101.
    • [2] Module 2: Internet Security Protocols: Specification and Modelling.
      Description of the NSPK protocol in HLPSL: pages 77 - 81.
    • [2] Module 4: Methods for Automated Protocol Analysis.
      More on the methodology of the AVISPA tool.
    • A Logic of Authentication.
      M. Burrows, M. Abadi, R. Needham.
      ACM Transactions on Computer Systems 8(1)(1990):18-36.