18-739 Foundations of Security and Privacy

References

Collections on protocols analysis

• A Survey of Authentication Protocol Literature: Version 1.0, John Clark, Jeremy Jacob
• Security Protocol Open Repository

Background Reading on SSL 3.0

• Analysis of the SSL 3.0 protocol, David Wagner, Bruce Schneier
• Finite-State Analysis of SSL 3.0, John Mitchell, Vitaly Shmatikov, Ulrich Stern
• Chosen Ciphertext Attacks against Protocols Based on RSA Encryption Standard PKCS #1, Daniel Bleichenbacher

RFCs and Internet-Drafts

• RFC2246 - The TLS Protocol Version 1.0
• Internet Key Exchange (IKEv2) Protocol
• List of current RFCs can be found here
• List of current Internet-Drafts can be found here

Contract signing protocols

• 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
• A Fair Protocol for Signing Contracts, Michael Ben-Or, Oded Goldreich, Silvio Micali, Ronald Rivest
• Analysis of Probabilistic Contract Signing, Gethin Norman, Vitaly Shmatikov

Protocols for Anonymity

• Untraceable Electronic Mail, Return addresses, and Digital Pseudonyms, David Chaum
• Free Haven Project Anonymity Bibliography
• The Cypherpunks Home Page
• Anonymity systems in various stages of deployment:
  • Mixminion: http://www.mixminion.net
  • Mixmaster: http://mixmaster.sourceforge.net
  • Anonymizer: http://www.anonymizer.com
  • Zero-Knowledge Systems: http://www.zeroknowledge.com

Probabilistic Model Checking

• Automatic Verification of Real-Time Systems with Discrete Probability Distributions, Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston
• Probabilistic Model Checking of an Anonymity System, Vitaly Shmatikov

Protocol Verification by the Inductive Method

• The Inductive Approach to Verifying Cryptographic Protocols, Lawrence Paulson
• Verifying Security Protocols Using Isabelle, a collection of case studies

Logic for Computer Security Protocols

• A Logic of Authentication, Michael Burrows, Martin Abadi, Roger Needham
• A Compositional Logic for Proving Security Properties of Protocols, Nancy Durgin, John Mitchell, Dusko Pavlovic
• A Derivation System for Security Protocols and its Logical Formalization, Anupam Datta, Ante Derek, John Mitchell, Dusko Pavlovic
• Protocol Composition Logic (PCL) by A. Datta, A. Derek, J. C. Mitchell, A. Roy
• Derivation of the JFK Protocol by Anupam Datta, John Mitchell, and Dusko Pavlovic
• Protocol Composition Logic web page

Symbolic Protocol Analysis

• 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

Security in Process Calculus

• A Calculus for Cryptographic Protocols: The Spi Calculus, Martin Abadi, Andrew Gordon
• Mobile Values, new Names, and Secure Communication, Martin Abadi, Cedric Fournet
• Reconciling Two Views of Cryptography, Martin Abadi, Phillip Rogaway
• A Probabilistic Polynomial-Time Calculus for Analysis of Cryptographic Protocols, John Mitchell, Ajith Ramanathan, Andre Scedrov, Vanessa Teague
• A Bisimulation Method for Cryptographic Protocols, Martin Abadi, Andrew Gordon

Game-Based Verification of Protocols

• Alternating-time Temporal Logic, Rajeev Alur, Thomas Henzinger, Orna Kupferman
• Mocha: Modularity in Model Checking, Rajeev Alur, Thomas Henzinger, F.Y.C. Mang, Shaz Qadeer, Sriram Rajamani, Serdar Tasiran
• A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols, Steve Kremer, Jean-Francois Raskin
• Game Analysis of Abuse-free Contract Signing, Steve Kremer, Jean-Francois Raskin

Software Model-Checking

• Modular Verification of Software Components in C by Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith

Cryptographic Soundness

• Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption by Martin Abadi and Phillip Rogaway)
• Soundness of Formal Encryption in the Presence of Active Adversaries by Daniele Micciancio, Bogdan Warinschi
• Probabilistic Polynomial-time Semantics for a Protocol Security Logic by A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, M. Turuani
• A Composable Cryptographic Library with Nested Operations (Extended Abstract) by Michael Backes, Birgit Pfitzmann, and Michael Waidner

Distributed Access Control

• Authentication in Distributed Systems: Theory and Practice by Butler Lampson, Martin Abadi, Michael Burrows, and Edward Wobber
• A Calculus for Access Control in Distributed Systems by Martin Abadi, Michael Burrows, Butler Lampson, and Gordon Plotkin
• Non-interference in Constructive Authorization Logic by Deepak Garg and Frank Pfenning
• Access Control in a Core Calculus of Dependency by Martin Abadi
• Proof-Carrying Authentication by Andrew W. Appel and Edward W. Felten

Privacy

• P3P Project Page
• The platform for privacy preferences by Joseph Reagle and Lorrie Faith Cranor
• EPAL Project Page
• A Privacy Policy Model for Enterprises by G. Karjoth, M. Schunter
• XACML Project Page
• Privacy as Contextual Integrity by H. Nissenbaum
• Privacy and Contextual Integrity: Framework and Applications by A. Barth, A. Datta, J. C. Mitchell, H. Nissenbaum
• Privacy and Utility in Business Processes by A. Barth, A. Datta, J. C. Mitchell, S. Sundaram

Language-based Security

• Language-Based Information-Flow Security by Andrei Sabelfeld, Andrew C. Myers
• Protecting Privacy using the Decentralized Label Model by Andrew C. Myers, Barbara Liskov
• Proof Carrying Code by George Necula
• The Design and Implementation of a Certifying Compiler by George C. Necula, Peter Lee
• CCured: type-safe retrofitting of legacy code by George C. Necula, Scott McPeak, Westley Weimer