| Meeting Date | Lecture | Reading/Lecture Slides | Hand-ins | ||
| Tue. 28-Aug-07 |
| Lecture: Course Overview
(pdf) CryptographyOverview (pdf) Optional: Cryptography Slides (pdf) Scribe Notes: Aakash Shah | |||
| Thu. 30-Aug-07 |
| Lecture: Model Checking (pdf) Reading: Automated Analysis of Cryptographic Protocols Using Murphi Scribe Notes: Luca Parolini | |||
| Fri. 01-Sep-07 | Murphi Lab - Room CIC 1301 2-4PM | CTL Model Checking(pdf)-David Dill Murφ:A Retrospective(pdf)-David Dill | |||
| Tue. 04-Sep-07 |
| Lecture: SSL (pdf) Reading: Finite-State Analysis of SSL 3.0 Scribe Notes: Shihong Ng |
| ||
| Thu. 06-Sep-07 |
| Lecture: JFK (pdf) Anonymity Protocols (pdf) Reading: Derivation of the JFK Protocol Untraceable Electronic Mail ... Dining Cryptographers ... Tor: The Second-Generation Onion Router Scribe Notes: Christopher Szilagyi | |||
| Fri. 08-Sep-07 | AVISPA Lab - Room CIC 1301 2-4PM | AVISPA Slides (pdf) | |||
| Tue. 11-Sep-07 |
| Lecture: Inductive Method (pdf) Reading: The Inductive Approach to Verifying Cryptographic Protocols | |||
| Thu. 13-Sep-07 |
| Lecture: BAN, PCL-I (pdf) Reading: Background in Logic: Sections 3.1-3.4 of Dynamic Logic by Harel, Kozen, Tiuryn Protocol Composition Logic (PCL) Optional: A Logic of Authentication, BAN slides (Harper) | |||
| Tue. 18-Sep-07 |
| Lecture: PCL-II (pdf) Reading: Protocol Composition Logic (PCL) (Section 6) Abstraction and Refinement in Protocol Derivation |
| ||
| Thu. 20-Sep-07 |
| Lecture: Applied Pi Calculus (pdf) Reading: Mobile values, New names, and Secure communication Optional: Just Fast Keying in the Pi Calculus Scribe Notes: Kumar Avijit | |||
| Fri. 21-Sep-07 | Prism Lab - Room CIC 1301 2-4PM | Probabilistic Model Checking for Security Protocols - Vitaly Shmatikov Grid-enabled Probabilistic Model Checking with PRISM - Zhang et. al. Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols - Ansgar Fehnker Parallel and Distributed Methods in Probabilistic Model Checker PRISM - Marta Kwiatkowska Probabilistic Model Checking of Randomised Distributed Protocols using PRISM - Dave Parker | |||
| Tue. 25-Sep-07 |
| Lecture: Model Checking C Code : Foundations Optional Reading: Predicate Abstraction: Construction of abstract state graphs with PVS Abstraction Refinement for C: Automatically Validating Temporal Safety | |||
| Thu. 27-Sep-07 |
| Lecture: Model Checking C Code : Security Applications Optional Reading: OpenSSL Verification: Modular Verification of Software Components in C | |||
| Tue. 2-Oct-07 |
| Proposals: See Blackboard |
| ||
| Thu. 4-Oct-07 |
| Proposals: See Blackboard | |||
| Tue. 9-Oct-07 |
|
Lecture: Correspondence Theorems (pdf) Reading: Soundness of Formal Encryption in the Presence of Active Adversaries Scribe notes: Jason Franklin | |||
| Thu. 11-Oct-07 |
|
Lecture: Computational Soundness for PCL (pdf) Reading: Probabilistic Polynomial-time Semantics for a Protocol Security Logic Scribe Notes: Ramu Panayappan | |||
| Tue. 16-Oct-07 |
|
Lecture: Distributed Access Control Overview Reading: An Introduction to Proof Carrying Authorization Authentication in Distributed Systems: Theory and Practice SPKI/SDSI Certificates SPKI Certificate Theory (RFC 2693) PGP (RFC 2440) Keynote Scribe Notes: Preston Mesick | |||
| Thu. 18-Oct-07 |
|
Lecture: Access Control in the Grey System Reading: Device-enabled Authorization in the Grey System Distributed Proving in Access-control Systems Scribe Notes: Napat Boonsaeng | |||
| Tue. 23-Oct-07 |
|
Lecture: Distributed Access Control Logics Reading: Constructive Authorization Logic Optional: ABLP Logic Scribe Notes: Deepak Garg | |||
| Thu. 25-Oct-07 |
|
Lecture: Trust Management Overview(pdf) Reading: Decentralized Trust Management Design of A Role-based Trust-management Framework Scribe Notes: Arvind Seshadri | |||
| Tue. 30-Oct-07 |
|
Lecture: RT and Distributed Credential Discovery (pdf) | |||
| Thu. 1-Nov-07 |
|
Lecture: Privacy Overview (pdf) Reading: Overview article in Stanford Encyclopedia of Philosophy Gavison's "Privacy and the Limits of Law" (no online version) Optional Reading: Protecting Respondents' Identities in Microdata Release Toward Privacy in Public Databases Scribe Notes: Michael Kaufman | |||
| Tue. 6-Nov-07 |
|
Lecture: EPAL Reading: EPAL Specification A Toolkit for Managing Enterprise Privacy Policies Scribe Notes: Michael Tschantz | |||
| Thu. 8-Nov-07 |
|
Lecture: Formalizing Contextual Integrity (pdf) Reading: Privacy and Contextual Integrity: Framework and Applications Privacy and Utility in Business Processes Optional Reading: Privacy as Contextual Integrity Scribe Notes: Evan Wright | |||
| Tue. 13-Nov-07 |
|
Lecture: Web site privacy using P3P (pdf) Reading: P3P Deployment on Websites Scribe Notes: Nathaniel Gist | |||
| Thu. 15-Nov-07 |
|
Lecture: Language-based Security Overview (pdf), Cyclone Reading: Cyclone: A safe dialect of C Type Systems (Sections 1-3) Mathematical Models of Computer Security (Section 5) Scribe Notes: Rupsha Chaudhuri |
HW2 out | ||
| Tue. 20-Nov-07 |
|
Lecture: Language-based Enforcement of Non-interference (pdf) Reading: Certification of programs for secure information flow A Sound Type System for Secure Flow Analysis Scribe Notes: Hayan Lee | |||
| Thu. 22-Nov-07 |
| ||||
| Tue. 27-Nov-07 |
|
Lecture: Jif Reading: Protecting Privacy using the Decentralized Label Model JFlow: Practical Mostly-Static Information Flow Control Secure web applications via automatic partitioning Scribe Notes: Rob Simmons | |||
| Thu. 29-Nov-07 |
| | |||
| Tue. 4-Dec-07 |
| HW2 due | |||
| Thu. 6-Dec-07 |
| Lecture: Course Review |
|