8:45 - 9:00 | Welcome Roberto Gorrieri (University of Bologna), General Chair Paul Syverson (Naval Research Laboratory), Program Chair |
9:00 - 10:00 | Formal Models Session Chair: Joshua Guttman (MITRE) A Formal Framework and Evaluation Method for Network Denial of Service PostScript, PDF Catherine Meadows (Naval Research Lab) I/O Automaton Models and Proofs of Shared-Key Communications Systems Nancy Lynch (MIT) |
10:00 - 10:30 | Break |
10:30 - 12:00 |
Security Protocol Analysis: Notation, Transformation, and Simplification Session Chair: Dieter Gollman (Microsoft Research) Safe Simplifying Transformations for Security Protocols Postscript Mei Lin Hui and Gavin Lowe (U. of Leicester) Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief PDF David Monniaux (École Normale Supérieure and SRI) A Meta-notation for Protocol Analysis Postscript I. Cervesato (Stanford U.), N.A. Durgin (Stanford U.), P.D. Lincoln (SRI), J.C. Mitchell (Stanford U.), and A. Scedrov (U. of Pennsylvania) |
12:00 - 2:00 | Lunch |
2:00 - 3:00 |
Strand Spaces Session Chair: John Mitchell (Stanford) Mixed Strand Spaces F. Javier THAYER Fabrega, Jonathan C. Herzog, Joshua D. Guttman (MITRE) Honest Functions and their Application to the Analysis of Cryptographic Protocols Al Maneki (National Security Agency) |
3:00 - 3:30 | Break |
3:30 - 5:00 | Panel: Formalization and Proof of Secrecy Properties Panel Chair: Dennis Volpano (Naval Postgraduate School) Panelists: Martín Abadi (Compaq SRC), Riccardo Focardi (U. Venezia - Ca' Foscari), Cathy Meadows (NRL), Jon Millen (SRI) |
9:00 - 10:00 |
Local Names Session Chair: Paul Syverson (NRL) Authentication via Localized Names Postscript Chiara Bodei (U. Pisa) , Pierpaolo Degano (U. Pisa), Riccardo Focardi (U. Venezia - Ca' Foscari), and Corrado Priami (U. Verona) A Logic for SDSI's Linked Local Name Spaces Joseph Y. Halpern (Cornell U.) and Ron van der Meyden (U. Tech. Sydney) |
10:00 - 10:30 | Break |
10:30 - 12:00 |
Interaction and Composition Session Chair: John McLean (Naval Research Lab) Trusted System Construction Colin O'Halloran (DERA) Secure Composition of Insecure Components Peter Sewell (Cambridge U.) and Jan Vitek (U. Genève) Security Function Interactions Postscript, Powerpoint Slides Pierre Bieber (ONERA CERT) |
12:00 - 2:00 | Lunch |
2:00 - 3:00 |
Logics for Authorization and Access Control Session Chair: Jon Millen (SRI) A Logic-based Knowledge Representation for Authorization with Delegation Ninghua Li (NYU), Joan Feigenbaum (AT&T Labs), and Benjamin Grosof (IBM) A Logical Framework for Reasoning on Data Access Control Elisa Bertino (U. Milano) , Francesco Buccafurri (U. Reggio Calabria), Elena Ferrari (U. Milano), and Pasquale Rullo (U. Calabria) |
3:00 - 3:30 | Break |
3:30 - 4:30 | CSFW Business Meeting |
9:00 - 10:00 |
Advances in Automated Security Protocol Analysis Session Chair: George Necula (UC Berkeley) Athena: A New Efficient Automatic Checker for Security Protocol Analysis Dawn Xiaodong Song (Carnegie Mellon U.) CVS: A Compiler for the Analysis of Cryptographic Protocols Gzipped Postscript Antonio Durante (U. Bologna), Riccardo Focardi (U. Venezia - Ca' Foscari), and Roberto Gorrieri (U. Bologna) |
10:00 - 10:30 | Break |
10:30 - 11:30 |
Noninterference Using Process Algebras Session Chair: Dennis Volpano (Naval Postgraduate School) Process Algebra and Non-interference Gzipped Postscript P Y A Ryan (DERA) and S A Schneider (U. London) What is intransitive noninterference? Gzipped Postscript A.W. Roscoe (Oxford U.) and M.H. Goldsmith (Formal System (Europe) Ltd.) |
11:30 - 12:00 | Closing remarks. Presentation of Bocce Awards |