18-739 — Foundations of Security and Privacy

Date

Topic

Reading

Notes

Tue Aug 25

No class—CS immigration course

Thu Aug 27

No class—CS immigration course

Tue Sep 1

No class—CS immigration course

Thu Sep 3

No class—CS immigration course

Tue Sep 8

Course Overview [PPT]
Cryptography: Cryptography Basic [PPT]

• CMU Computing Policy
• CMU Policy on Cheating

Thu Sep 10

Bug Finding: Model Checking: Overview and the Murphi tool [PPT ]

• Automated Analysis of Cryptographic Protocols Using Murphi [PS]
• Optional: Securing Frame Communication in Browsers [PDF]

Tue Sep 15

Bug Finding: Model checking: SSL/TLS Case Study [PPT]

• Finite-State Analysis of SSL 3.0 [PS]
• Optional: Short Chosen-Prefix Collisions for MD5 and the Creation of a Rogue CA Certificate [PDF]

Murphi (gcc 4.2.x) [Murphi3.1_gcc4.2.zip]

Murphi (gcc 4.3.x) [Murphi3.1_gcc4.3.zip]

HW 1 handed out [PDF]

Model Files [hw1.zip]

Thu Sep 17

(Dilsun Kaynar)

Protocol Examples:
JFK-Anonymity [PPT]

• Derivation of the JFK Protocol [PS]
• Untraceable Electronic Mail ... [PDF]
• Dining Cryptographers ...
• Tor: The Second-Generation Onion Router [PDF]

Tue Sep 22

Proving Security: Protocol Logics: BAN, Protocol Composition Logic (PCL) I [PPT]

• Background in Logic: Sections 3.1-3.4 of Dynamic Logic by Harel, Kozen, Tiuryn
• Protocol Composition Logic (PCL) [PDF]
• A Logic of Authentication [PDF]
• BAN slides (Harper) [PDF]

Tue Sep 29

Proving Security: Protocol Composition Logic (PCL) II [PPT]

• Protocol Composition Logic (PCL) (Section 6) [PDF]
• Abstraction and Refinement in Protocol Derivation [PS]

HW 1 due today 12:01 AM

Thu Oct 1

Introduction to Computational Cryptography [PPT]

• Bellare-Rogaway Lecture Notes:
  Chapter 1: [PDF]
• Chapter 4: [PDF]

HW 2 handed out [PDF]

LaTex source of the HW PDF [PDF]

Tue Oct 6

Cryptographic Soundness I [PDF]

Cryptographic Soundness Proof [PPT]

• Reconciling Two Views of Cryptography
  (The Computational Soundness of Formal Encryption)
  [PDF]

Thu Oct 8

Cryptographic Soundness II [PPT]

• Inductive Trace Properties for Computational Security [PDF]
• Optional : Soundness of Formal Encryption in the Presence of Active Adversaries [PDF]

Project Proposal due today

Tue Oct 13

Privacy: Overview [PPT]

• Overview article in Stanford Encyclopedia of Philosophy
• Gavison's "Privacy and the Limits of Law" (no online version)
• Protecting Respondents' Identities in Microdata Release [PDF]

HW 2 due today before class

HW 3/Mid Sem handed out [PDF]

Thu Oct 15 (*)

Privacy: Database Privacy [PPT] [PDF]

• Differential Privacy [PDF]
• Robust De-anonymization of Large Sparse Datasets (How to Break Anonymity of the Netflix Prize Dataset) [PDF]

HW 3/Mid Sem due before class

Tue Oct 20 (*)

Privacy: Contextual Integrity & LPU [PPT]

• Privacy and Contextual Integrity: Framework and Applications [PDF]
• Privacy and Utility in Business Processes [PDF]

HW 4 handed out [PDF]

Thu Oct 22

(Lorrie Cranor)

Privacy: P3P [PDF]

• L. Cranor, S. Egelman, S. Sheng, A. McDonald, and A. Chowdhury. P3P Deployment on Websites. Electronic Commerce Research and Applications, 2008. [HTML]
• S. Egelman, J. Tsai, L. Cranor, and A. Acquisti. 2009. Timing Is Everything? The Effects of Timing and Placement of Online Privacy Indicators. CHI '09: Proceedings of the SIGCHI conference on Human Factors in Computing Systems. [PDF]
• P. Kelley, J. Bresee, L. Cranor, and R. Reeder. A "Nutrition Label" for Privacy. SOUPS 2009 [PDF]

Tue Oct 27

(Deepak Garg)

Language-based Security: Overview [PDF]

• Mini-C [PDF]
• Type Systems (Sections 1-3) [PDF]
• Cyclone: A safe dialect of C [PDF]

Thu Oct 29

(Karl Crary)

Language-based Security: Certifying Compilation

• From System F to Typed Assembly Language [PDF]

Tue Nov 3

Language-based Security: Information Flow [PPT]

• Mathematical Models of Computer Security (Section 5) [PDF]
• A Sound Type System for Secure Flow Analysis [PDF]
• Certification of programs for secure information flow

Thu Nov 5

(Deepak Garg)

Decentralized Access Control: Overview [PDF]

• Sections 1 and 2 of Authentication in Distributed: Theory and Practice Systems [PDF]
• Keynote
• Lampson's Protection paper [PDF]
• Optional: SPKI Certificate Theory (RFC 2693)
• Optional: PGP (RFC 2440)
• Optional: X.509

HW 4 due today 10:35 AM

HW 5 handed out [PDF]

Tue Nov 10

(Deepak Garg)

Decentralized Access Control: Logics [PDF]

• Access Control Logic: Notes [PDF]
• SecPAL: (Sections 1-6) [PDF]
• Access Control Logics [PDF]
• Optional : Constructive Authorization Logic [PDF]
• Optional : Proof theory of Intuitionistic Logic [PDF1   PDF2 ]

Thu Nov 12

(Lujo Bauer)

Distributed Access Control: Grey System Case Study [PDF]

• Device-enabled Authorization in the Grey System [PDF]
• Distributed Proving in Access-control Systems [PDF]

Tue Nov 17 (Jeremiah Blocki)

Advanced Topics and Current Research [PPT]

HW 5 due today 10:35 AM

Thu Nov 19 (Limin Jia)

Advanced Topics and Current Research [PDF]

Tue Nov 24 (Deepak Garg)

Advanced Topics and Current Research [PDF]

Thu Nov 26

No class—university holiday

Tue Dec 1 (Students)

Project presentations

Project models/code due today 12:01 AM

Project report (5-10 pages) due today 12:01 AM

Thu Dec 3 (Students)

Project presentations/Wrap up

HW 6/End Sem handed out (due Tue Dec 8)