Course outline, Computer security, Cryptographic protocols, Security analysis, Needham-Schroeder example, Murphi.
Resources:
· A Survey of Authentication Protocol Literature: Version 1.0, John Clark, Jeremy Jacob
· Security Protocol Open Repository
Encryption Schemes: symmetric key and public key, Hash functions, Signature Schemes, Simple examples and constructions.
Resources:
·
Handbook
of Applied Cryptography, Alfred J. Menezes, Paul C. van Oorschot and Scott A. Vanstone
Starting with the RFC describing the protocol, how to create an abstract model and code it up in Murphi, specify security properties, and run Murphi to check whether security properties are satisfied.
Resources:
· Finite-State Analysis of SSL 3.0, John Mitchell, Vitaly Shmatikov, Ulrich Stern
Running Murphi in various environments, overview of the method, discussion on the Needham-Schroeder example code.
Resources:
· Murphi User Manual, Ralph Melton, David L. Dill, updated by C. Norris Ip and Ulrich Stern
Key management, Kerberos, Public-Key infrastructure, Security properties and attacks on them, Diffie-Hellman key exchange, IPSEC, IKE.
Contract-Signing and Fair-Exchange, Trusted third party, Optimistic Contract-Signing, Asokan-Shoup-Waidner protocol, Desirable properties (fairness, timeliness, accountability, balance), Abuse-Free Contract-Signing.
Resources:
·
Optimistic
Protocols for Fair Exchange, N. Asokan, Matthias Schunter, Michael Waidner
·
Abuse-free Optimistic
Contract Signing, Juan Garay, Markus Jakobsson, Philip MacKenzie
· Finite-State Analysis of Two Contract Signing Protocols, Vitaly Shmatikov, John Mitchell
Proving protocols secure, Symbolic model, Challenge Response example, Informal hand proof, Formalization in PCL language, syntax, semantics, proof rules, Example proof of security in PCL.
Resources:
· Protocol composition logic (PCL), by Anupam Datta, Ante Derek, John C. Mitchell and Arnab Roy
Lecture 6b. Proving IEEE
802.11i Secure:
802.11i Key Management, Security properties of TLS, PCL proof structure and sketches, Interaction flaws.
Resources:
· A Modular Correctness Proof of TLS and IEEE 802.11i (shorter conference version), by Changhua He, Mukund Sundararajan, Anupam Datta, Ante Derek, and John C. Mitchell
· A Modular Correctness Proof of IEEE 802.11i and SSL / TLS (longer version in review), by Changhua He, Mukund Sundararajan, Arnab Roy, Anupam Datta, Ante Derek, and John C. Mitchell
· Security Analysis and Improvements for IEEE 802.11i, Changhua He and J.C. Mitchell
· Analysis of the 802.11i 4-Way Handshake, Changhua He and J.C. Mitchell
XOM architecture, Software distribution model, Security specifications, Modeling and security analysis in Murphi.
Resources:
· Specifying and Verifying Hardware for Tamper-Resistant Software, by D. Lie, J. Mitchell, C. Thekkath, M. Horowitz
· Architectural Support for Copy and Tamper Resistant Software by D. Lie, C. Thekkath, P. Lincoln, M. Mitchell, D. Boneh, J. Mitchell, M. Horowitz
Brief descriptions of protocols/systems to be analyzed by students.
Dining Cryptographers, Definitions of Anonymity, Onion Routing, Crowds System.
Probabilistic Model Checking, PRISM, PCTL (logic).
Probabilistic Contract Signing, Properties of Probabilistic Fair Exchanges, Rabins Beacon, BGMR Probabilistic Contract Signing, Formal Model.
Slides: [ppt][pdf]
Resources:
· Crowds: Anonymity for Web Transactions, by Michael K. Reiter and Aviel D. Rubin
· PCTL: A Logic for Reasoning about Time and Reliability, by Hans Hansson and Bengt Jonsson
· Analysis of Probabilistic Contract Signing, by Gethin Norman and Vitaly Shmatikov
· Probabilistic Model Checking of an Anonymity System, by Vitaly Shmatikov
How to go about doing your CS259 project, Modeling the protocol, Analysis in MOCHA, Attacks found.
Slides: [ppt][pdf]
Resources:
· An Anonymous Fair Exchange E-commerce Protocol, by Indrakshi Ray and Indrajit Ray
· CS259 Project page of Adam Barth and Andrew Tappert
Complexity of proving security properties, Protocol analysis techniques, Strand Spaces, Constraint Solving: SRI Constraint Solver and Prolog.
Slides: [ppt][pdf]
Resources:
· Strand Spaces: Why is a Security Protocol Correct?, Joshua Guttman, Jonathan Herzog, Javier Thayer
· Constraint Solving for Bounded-Process Cryptographic Protocol Analysis, Jonathan Millen, Vitaly Shmatikov
· Constraint Solving in Prolog
Formal description of security properties of the protocols/systems to be analyzed, tools to be used.
Analysis by theorem proving, Inductive proofs, Protocol traces, Dolev-Yao attacker model.
Slides: [ppt][pdf]
Resources:
·
The Inductive Approach to Verifying Cryptographic
Protocols, by
Floyd-Hoare logic of programs, BAN logic, PCL.
Slides: [ppt][pdf]
Resources:
· An axiomatic basis for computer programming, by C. A. R. Hoare
· A Logic of Authentication, by Michael Burrows, Martνn Abadi, Roger Needham
Intuition, Formalization: protocol specification language, syntax, semantics, proof system, Protocol composition, Complexity theoretic semantics.
Slides: [ppt][pdf]
Resources:
· Protocol composition logic (PCL), by Anupam Datta, Ante Derek, John C. Mitchell and Arnab Roy