Logics in Security

MPI-SWS/Saarland University
Winter 2014

Time: Twice a week, Wednesday, 14:15-15:45 and Thursday, 10:30-12:00
Location: E1.5 Room 029 (SB) videocast to 112 (KL)

Instructor: Deepak Garg. Email: Click to reveal email

Language: English

Overview

This course will explore applications of logics in security. Topics include protocol verification with tools like ProVerif, authorization logics (special modal logics), logics in privacy, and a selection of logics used for proving security properties of programs. This course is intended for graduate and advanced undergraduate students. This is NOT a standard seminar. Scroll down to understand how the course is structured.

Homeworks

• Homework 4 [PDF, TeX] Release: 02.02.15, Due: 14.02.15, Discussion: 04.03.15, Redo due: 07.03.15
• Homework 3 [PDF, TeX] Release: 13.12.14, Due: 20.12.14, Discussion: 08.01.15, Redo due: 16.01.15
• Homework 2 [zip, tar/gz] Release: 01.12.14, Due: 08.12.14, Discussion: 10.12.14, Redo due: 13.12.14
• Homework 1 [PDF, TeX] Release: 12.11.14, Due: 19.11.14, Discussion: 03.12.14, Redo due: 06.12.14

Schedule

The schedule given below is tentative and will be updated as the class progresses. This schedule is NOT in chronological order. It is organized by modules. For copyright reasons, links to papers are password-protected. If you are in the class, you should have received an email with the login and password. If not, send an email to the class instructor.

Module 1: Security properties Basic paper: Enforceable Security Properties. Fred Schneider. TISSEC 2000. Advanced papers: Hyperproperties. Michael Clarkson and Fred Schneider. CSF 2008. Runtime Enforcement of Security Policies on Black Box Reactive Programs. Minh Ngo, Fabio Massacci, Dimiter Milushev and Frank Piessens. POPL 2015.
October 29	In-class discussion: Basic paper	PDF
October 30	Basic paper clarifications	Recommended reading: Advanced paper 1, Sections 1-3. [PDF]
November 12	Advanced paper presentations Presenters: Vineet Rajani, Adam Smith	Homework 1 out, due on November 19. [PDF, TeX source]
December 3	Homework 1 solution discussion Presenter: Iulia Bolosteanu	Homework 1 redo due on December 6
Module 2: ProVerif Basic paper: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. Bruno Blanchet. CSFW 2001. Background reading on cryptographic protocols: Prudent engineering practice for cryptographic protocols. Martin Abadi and Roger Needham. IEEE TSE, 1996. Applied Cryptography. Bruce Schneier. Chapters 1-3. This book is available online, just Google for it. Advanced papers: Analyzing Security Protocols with Secrecy Types and Logic Programs. Martin Abadi and Bruno Blanchet. JACM 2005. Automatic Verification of Correspondences for Security Protocols. Bruno Blanchet. arXiv:0802.3444 2008.
November 5	Introduction to judgments, deduction, induction	Frank Pfenning's LP lecture notes, Chapters 1, 3. [PDF]
November 6	Backchaining and unification	Frank Pfenning's LP lecture notes, Chapter 1. [PDF]
November 13	In-class discussion: Basic paper	PDF
November 19	Inductive proofs	Frank Pfenning's LP lecture notes, Chapter 3. [PDF]
November 20	Prolog, ProVerif semantics	Frank Pfenning's LP lecture notes, Chapters 4, 5, 6. [PDF] Basic paper, Figure 4. [PDF]
December 1	--	Homework 2 out, due on December 8. [.zip, .tgz]
December 10	Homework 2 solution discussion Presenter: Iulia Bolosteanu	Homework 2 redo due on December 13
Module 3: Authorization logics Basic paper: Design and Semantics of a Decentralized Authorization Language. Moritz Becker, Cedric Fournet and Andrew D. Gordon. CSF 2007. Advanced papers: Noninterference in Constructive Authorization Logic. Deepak Garg and Frank Pfenning. CSFW 2006. Access Control in a Calculus of Core Dependency. Martin Abadi. ICFP 2006.
November 26	Intuitionistic logic: Hypothetical judgments and natural deduction	Frank Pfenning's ATP lecture notes, Sections 2.1, 2.3. [PDF]
November 27	Local soundness, completeness and substitution	Frank Pfenning's ATP lecture notes, Sections 2.1, 2.3. [PDF]
December 4	In-class discussion: Basic paper	PDF
December 10	Tabled logic programming	Basic paper, Section 7. [PDF]
December 13	--	Homework 3 out, due on December 20. [PDF, TeX source]
January 8	Homework 3 solution discussion	Homework 3 redo due on January 16
Module 4: Information flow Basic paper: A Sound Type System for Secure Flow Analysis. Dennis Volpano, Geoffrey Smith and Cynthia Irvine. JCS 1996. Advanced papers: On Flow-Sensitive Security Types. Sebastian Hunt and David Sands. POPL 2006. A Core Calculus of Dependency. Martin Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke. POPL 1999. Information Flow Inference for ML. Francois Pottier and Vincent Simonet. POPL 2002.
December 11	Reduction (small-step) semantics for an imperative language
December 17	Type systems
December 18	Type safety
January 7	Big-step semantics
January 28	In-class discussion: Basic paper	PDF
January 29	Detailed discussion of basic paper	PDF
February 2	--	Homework 4 out, due on February 14. [PDF, TeX source]
March 4	Homework 4 solution discussion Presenter: Iulia Bolosteanu	Homework 4 redo due on March 7
Module 5: Security for effects Basic paper: This module has no basic paper. We'll cover all basic material in class. Advanced papers: A Type Discipline for Authorization Policies. Cedric Fournet, Andrew D. Gordon and Sergio Maffeis. TOPLAS 2007. Refinement Types for Secure Implementations. Jesper Bengtson, Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon and Sergio Maffeis. CSF 2008. Logical Foundations of Secure Resource Management in Protocol Implementations. Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, Matteo Maffei. POST 2013.
February 4	Untyped lambda calculus	B.C. Pierce's TAPL book, Chapter 5
February 5	Encoding data structures, recursion in the lambda calculus	B.C. Pierce's TAPL book, Chapter 5
February 12	Simple types for the lambda calculus	B.C. Pierce's TAPL book, Chapter 9
February 18	Type safety for the lambda calculus	B.C. Pierce's TAPL book, Chapter 9
February 25	Types for correspondence properties

Course structure

The course is structured as a hybrid of a seminar and an advanced lecture. What this means is that students can learn from the course independent of their existing background in logic and security. The course is structured into several modules. Each module teaches one application of logic in security. Each module lasts for approximately 2 weeks (4 class meetings) and is based on 3-4 papers, of which one is a basic paper and the rest are advanced papers. The modules are independent of each other, although they progressively teach you more and more advanced techniques in logic. Each module works as follows:

• Before the first meeting of the module, everyone reads the module's basic paper and prepares a list of discussion questions.
• 1st meeting: In-class discussion on the basic paper. At the end of the meeting, each student decides (independently) whether she/he wants to read the advanced papers (the "S" track) or requires more background to understand the basic paper (the "L" track).
• 2nd and 3rd meetings: What you do in these meetings depends on whether you chose the S track or the L track.
  • L track: The instructor will teach lectures on fundamental topics (logic, process calculi, type systems, etc.) to help you understand the basic paper fully.
  • S track: You stay at home, read the 2-3 advanced papers of the module and write summaries of those papers.
• 4th meeting: Two selected students from the S track give 30 minute presentations on two separate advanced papers. All students attend.
• Follow up: After the 4th meeting, the S track students turn in their paper summaries. The L track students get a homework, which evaluates their learning of the basic lectures and the basic paper.

This process repeats for each module. Students are free to switch S and L tracks independently for each module. Note that the S track is considerably more flexible than the L track (you attend only the first and last meetings of the module in the S track) and allows you learn more, so you should not choose the L track unless you really need the background.

Grading

Each module is graded independently. The total grade is the sum of grades in all modules. There is no final exam. The criteria for your grade in a module depends on the track you choose in the module:

• L track: Participation in all meetings and homework.
• S track: Participation in the first and last meetings, paper summaries and class presentation (whenever you do that).

Here, participation means not just attendance but also asking sensible questions (however elementary).

Homeworks

Homeworks will evaluate your technical understanding of the subject matter. They may ask for proofs or examples. All homeworks are open book and open discussion. You can talk to anyone about the homework. However, you are not allowed to take any written notes from any discussion about the homework. The intent of this policy is to promote collaborative learning, yet ensure that every person reconstructs every solution in its entirety at least once. Homework discussions over persistent written media (email, text, IM) are prohibited. Homeworks are due on a pre-determined date.

Paper summaries

For each advanced paper in the module, turn in a one page technical summary of the paper. You are encouraged to critique specific points, ideas, axioms and theorems in each paper. What we do not want are high-level summaries of the main ideas only. There is no need to summarize the basic paper. Summaries are due by email before the end of the day of the final meeting of the module and must be typeset.