Course
on
Linear Logic and Security
June 15-26, 2003
Summer
School on Foundations of Security
Eugene, OR - USA
Syllabus
Powerpoint slides are available for each lecture. They can be accessed by
clicking on their title.
Lecture 1: Basics
[ppt]
- Multiset rewriting
- Monoids
- Multisets
- Transitions
- Petri nets
- Traces
- Sequential vs. trace semantics
- Linear logic
- Conjunctive / disjunctive encoding
Lecture 2: Multiset Rewriting for Protocols
[ppt]
- First-order multiset rewriting
- Generating data
- Colored Petri nets and first-order linear logic
- Cryptographic protocols
- Dolev-Yao model of security
- MSR 1.0
- Protocol representation
- Intruder
- Decidability and complexity
Lecture 3: Comparison and Encodings
[ppt]
- How does MSR compare with other languages?
- Strand spaces
- Dynamic strands
- Canonical MSR to dynamic strands
- Decorated strands to MSR
- Relations to linear logic
- Strand spaces to linear logic
Lecture 4: MSR 2.0
[ppt]
- Is MSR any good in practice?
- Extension and rationalization
- MSR 2.0
- Typing infrastructure
- Execution model
Lecture 5: Data Access Specification
[PS,
ppt]
- Data Access Specification (DAS)
- The MSR 2.0 notion of attacker
- Generic attacker
- Completeness of the Dolev-Yao intruder
- "The wolf within" (DAS vs. PDY)
- Distilling PDY from DAS
- Annotated protocol specifications
- Knowledge Evaluation Specification
Lecture 6: Verification of Kerberos 5
[ppt]
- Security protocol verification
- Kerberos 5
- Main exchange
- MSR 2.0 formalization
- Abstract / detailed specification
- Proof method
- Rank / corank functions
- General approach
- Verification of Kerberos 5
- Authentication properties
- Anomalies
Lecture 7: Towards MSR 3.0
[ppt]
Lecture 8: A Concurrent Logical Framework
[ppt]