Use TulaFale to implement and verify an interesting web service.
Research the various notions of behavioral equivalences for some simple variant of the pi-calculus. Write a summary of your findings. Include some examples and outline the proof for proving at least one of the equivalences you discuss.
Use a language based on one of the process calculi (e.g, PICT, JoCaml, LySa) and implement a few security protocols.
Research the use of continuations in web servers. Write a description of the problems that continuations are supposed to solve, how well they solve them, and what are the problems associated with the use of continuations. Support your narrative with code (or pseudo-code) from a web server implemented using continuations.
Design or find an interesting (non-trivial) XML document format. Use XDuce (or a similar typed XML processing language) to write a few programs that process your documents.
Part I: Take the subset of XML values and schemas introduced in "The Essence of XML" and implement matching, erasure, validation, and optimized matching.
Part II: Extend your implementation with at least one additional construct from the full XML/Schema definition.
Prove the two main theorems in "The Essence of XML:" Validation (Theorem 1), Sensibility (Theorem 2).
Date | Topic | Presenter |
11 Jan | Introduction | |
13 Jan | What is a web service? | Adam |
18 Jan | The Essence of XML | |
20 Jan | No class | |
25 Jan | Type theory: subtyping, polymorphism | |
27 Jan | Parametric Polymorphism for XML, XDuce | |
1 Feb | No class | |
3 Feb | No class | |
8 Feb | SOAP | Joseph |
10 Feb | WSDL | Satoshi |
15 Feb | Security primitives | Sid |
17 Feb | Security primitives (continued) | Sid |
22 Feb | The Spi calculus | |
24 Feb | Security: Overview and experience | Liang and Alek |
1 Mar | Tools demo: ProVerif and Samoa | Chun-Yu |
3 Mar | Observational Equivalence; Bisimilarity | |
8 Mar | Validating a web service security abstraction by typing | Corey |
10 Mar | ||
15 Mar | Spring break | |
17 Mar | Spring break | |
22 Mar | Discussion of final projects | |
24 Mar | Compiling web services to the spi-calculus | |
29 Mar | The breaking of SHA1 | Nathan |
31 Mar | Hoare logic | Gate |
5 Apr | Hoare logic | |
7 Apr | TLS and Isabelle | |
12 Apr | Modeling Services in the spi-calculus | |
14 Apr | WS-Security Policies | Wei |
19 Apr | SXML | Chris |
21 Apr | Modeling Services in the spi-calculus | Adam |
26 Apr | Ahmet and Ali | |
28 Apr |