Instructor	Dominique Unruh <surname (at) mmci (dot) uni-saarland (dot) de>
Mailing list	fmc09@mail-infsec.cs.uni-sb.de (subscribe/archive)
Lecture Period	October 13, 2009 - February 4, 2010
Lectures	Tuesday, 10:15-12:00am, room: HS003
Tutorials	Thursday, 10:15-12:00am, room: SR015
Course Material	Photos of black board, mininotes (split lecture-wise)
Language	English
Exam	Oral; 6 ECTS
Contact	Dominique Unruh <surname (at) cs (dot) uni-sb (dot) de>

News

• No lecture on Tue, Jan 26. On Thu, Jan 28 there will be a lecture instead of a tutorial.
  
• HISPOS registration due on December 3.
  
• No lecture on Tue, Nov 10. No tutorial on Thu, Nov 12.
  

Topics covered

2009-10-13 (lecture)	Overview: What is the Dolev-Yao approach, what is the cryptographic approach? Motivation for computational soundness results.
2009-10-15 (tutorial)	How do define a symbolic model. How to model active attackers in the DY-model.
2009-10-20 (lecture)	Where the Dolev-Yao approach fails: examples for symbolic models that are not computationally sound.
2009-10-22 (tutorial)	How to prove security in the symbolic setting? Rule induction.
2009-10-27 (lecture)	Inference rules & induction. Definition: symbolic model.
2009-10-29 (tutorial)	Modeling public key encryption.
2009-11-03 (lecture)	Passive computational soundness of symmetric encryption: definitions and begin of proof.
2009-11-05 (tutorial)	Definition: correctness of a computational implementation in the passive case.
2009-11-17 (lecture)	Passive computational soundness of symmetric encryption: missing conditions and finished proof.
2009-11-19 (tutorial)	How to model protocols in SPASS? Why length-regularity is important?
2009-11-24 (lecture)	Modeling protocols (active symbolic setting; CoSP).
2009-11-26 (tutorial)	Examples of CoSP protocols. Node traces of these protocols.
2009-12-01 (lecture)	Computational execution of CoSP protocols. Definition of computational soundness (active case; CoSP). High-level overview of computational soundness proofs in CoSP.
2009-12-03 (tutorial)	How to define a CoSP simulator for the case of public key encryption (definition of the translation functions β and τ).
2009-12-08 (lecture)	Required properties of a CoSP simulator. Definition of simulator for public key encryption.
2009-12-10 (lecture)	Proof: Indistinguishability of the simulator.
2009-12-15 (lecture)	Proof: Simulator is Dolev-Yao style. Theorem: Computational soundness of public key encryption.
2009-12-17 (tutorial)	[I forgot]
2010-01-05 (lecture)	Sequences of games. Calculus used by CryptoVerif (simplified version without arrays).
2010-01-07 (tutorial)	Design of transformation rules for the CryptoVerif calculus.
2010-01-12 (lecture)	Transformations used by CryptoVerif.
2010-01-14 (tutorial)	Symbolic models for blind signatures and zero-knowledge (special case).
2010-01-19 (lecture)	Symbolic model for zero-knowledge.
2010-01-21 (tutorial)	Example of more complex symbolic ZK-proof. Why is the normal definition of soundness of proof systems too weak for computational soundness?
2010-01-28 (lecture)	Extraction zero-knowledge. Computational Implementation for zero-knowledge.
2010-02-02 (lecture)	Proof sketch for computational soundness of zero-knowledge proofs.
2010-02-04 (tutorial)	Modeling of anonymity. Statical equivalence.

Homework

Your current amount of points in homework and tutorial can be accessed here.

Out / due	Homework	Solution
2009-10-22 / 2009-11-03	Homework 1	Solution 1
2009-10-05 / 2009-11-17	Homework 2	Solution 2, SPASS
2009-11-19 / 2009-12-08	Homework 3	Solution 3
2009-12-15 / 2010-01-05	Homework 4	Solution 4
2010-01-14 / 2010-01-28	Homework 5, CryptoVerif	Solution 5, CryptoVerif

Description

In the early 1980s, two separate and largely disjoint schools of thought have emerged in the field of secure protocol design and analysis, the cryptography community, and the formal methods community.

The formal methods (FM) community models protocol messages as symbolic terms, a somewhat unrealistic but highly useful idealization. This idealization enables automated analysis of very complex protocols and is applicable to real-life systems. This modeling, however, is frowned upon by the cryptographers as being extremely unrealistic and thus not meaningful.

The cryptographers, on the other hand, employ a much more realistic modeling in which messages are sequences of bits and cryptographic algorithms (such as encryption) are polynomial-time algorithms. This model is close to reality. The FM community, however, frowns upon the cryptographers: Due to the complexity of the modeling, the cryptographers can only analyze small toy-protocols.

In this lecture, I will try to bring unity into a divided world. I will present so-called computational soundness results that allow to derive security in the cryptographers’ models using the FM community’s tools, thus getting the best of two worlds.

Possible topics include:

• (Short) introduction to "symbolic crypto" and "computational crypto" (the two viewpoints)
• Why symbolic crypto fails – some examples how things go wrong
• Computational soundness theorems: when symbolic crypto is "the right thing to do"
• Computational soundness of zero-knowledge proofs – beyond just encryptions and signatures
• Observational equivalence: towards properties like anonymity and incoercibility

Related Lectures

The lectures "Cryptography" and "Advanced Cryptography" by Prof. Backes focus on the cryptographers' view-point, and the lecture "Language-based Security" by Matteo Maffei concentrates on the formal methods aspect. Attendence of these lectures is not required, but in particular the "Language-based Security" lecture nicely complements my lecture.

Prerequisites

It is recommended that you have heard a lecture on cryptography, for example one of Prof. Backes’ lectures.