Logics in Security
MPISWS/Saarland University
Winter 2014
Time: Twice a week, Wednesday, 14:1515:45 and
Thursday, 10:3012: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
passwordprotected. 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 
Inclass discussion: Basic paper

PDF

October 30 
Basic paper clarifications

Recommended reading: Advanced paper 1, Sections 13. [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 
Inclass 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 
Inclass 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 (smallstep) semantics for an imperative language


December 17 
Type systems


December 18 
Type safety


January 7 
Bigstep semantics


January 28 
Inclass 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 34 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: Inclass 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 23 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 predetermined 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 highlevel 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.