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

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: Advanced papers:
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: Background reading on cryptographic protocols: Advanced papers:
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: Advanced papers:
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: Advanced papers:
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:
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: 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: 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.