 |
|
||||||||||
Course Material for FMsec 09
Master in Information Security
For more information about the Information Security Master Track visit: http://www.infsecmaster.ethz.ch
Lecture Slides and Exercises
| Date | Lecture | Exercises | Solutions |
| 21.09. |
Introduction [pdf] |
None. |
None. |
| 28.09. |
Security Protocols I: Introduction (v3, 6.10.) [pdf] |
Exercise 1 [pdf] |
Solution 1 [pdf] |
|
05.10. |
Security Protocols II: Syntax and Operational Semantics (v2, 6.10.) [pdf] |
Exercise 2 [pdf] |
Solution 2 [pdf]
(v2, 13.10.) |
|
12.10. |
Security Protocols III: Operational Semantics and Security Goals (v2, 19.10.) [pdf] |
Exercise 3 [pdf] |
Solution 3 [pdf]
(v2, 20.10.) |
|
19.10. |
Security Protocols IV: Algorithmic Analysis Methods (Part 1) [pdf] |
Exercise 4 [pdf] |
Solution 4 [pdf] |
|
26.10. |
Security Protocols V: Algorithmic Analysis Methods (Part 2) (v2, 10.02.10) [pdf] |
Exercise 5 [pdf] |
Solution 5 [pdf] |
|
2.11. |
Security Protocols VI: Deductive Analysis Methods (Part 1) (v2, 9.11.09) [pdf] |
Exercise 6 [pdf] |
Solution 6 [pdf]
(v2, 10.11.) |
|
9.11. |
Security Protocols VII: Deductive Analysis Methods (Part 2) |
Exercise 7 [pdf]
(v2, 12.11) |
Solution 7 [pdf] |
|
16.11. |
Security Protocols VIII: Channels and Composition [pdf] |
Exercise 8 [pdf] |
Solution 8 [pdf] |
|
23.11. |
Security Protocols IX: Computational Soundness of Formal Encryption (v2, 24.11.) [pdf] |
Exercise 9 [pdf] |
Solution 9 [pdf] |
|
30.11. |
Non-interference (v2, 1.12.) [pdf] |
Exercise 10 [pdf] |
Solution 10 [pdf] |
|
7.12. |
Information Flow [pdf] |
Exercise 11 [pdf] |
Solution 11 [pdf] |
|
14.12. |
Review and Wrap-up (including Questions & Answers) |
Papers
- John Rushby, Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-02. Computer Science Laboratory, SRI International, Menlo Park, CA, 1992. [pdf]
OFMC Tool
We will use the Open source Fixedpoint Model-Checker v.2009 for the exercises.
- The source distribution (including examples) is available here [zip]. If you want to compile OFMC from sources you need the Haskell Platform.
- Please use these updated binaries for Linux, Mac OS X, and Windows (v2009b, Oct 13).
Remarks regarding version v2009b of OFMC
- The default for typing is now "-typed". Use "-untyped" to find type flaw attacks.
- There are new goal specifications supplementing those in channel notation.
- Secrecy: "M secret between A, B, C"
- Authentication: "A [weakly] authenticates B on M"
- Weak/strong authentication = Non-injective/injective agreement (see lecture)
- "B *-> A: M" = "A authenticates B on M" (strong authentication)
Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne
graphische Elemente dargestellt. Die Funktionalität der
Website ist aber trotzdem gewährleistet. Wenn Sie diese
Website regelmässig benutzen, empfehlen wir Ihnen, auf
Ihrem Computer einen aktuellen Browser zu installieren. Weitere
Informationen finden Sie auf
folgender
Seite.
Important Note:
The content in this site is accessible to any browser or
Internet device, however, some graphics will display correctly
only in the newer versions of Netscape. To get the most out of
our site we suggest you upgrade to a newer browser.
More
information
!!! Dieses Dokument stammt aus dem ETH Web-Archiv und wird nicht mehr gepflegt !!!
!!! This document is stored in the ETH Web archive and is no longer maintained !!!
!!! This document is stored in the ETH Web archive and is no longer maintained !!!
