12th IEEE Computer Security Foundations Workshop

June 28-30, 1999

Mordano, Italy

Sponsored by the IEEE Computer Society

Report on the Workshop by Scott Stoller

Technical Program

MONDAY June 28, 1999

8:45 - 9:00Welcome
Roberto Gorrieri (University of Bologna), General Chair
Paul Syverson (Naval Research Laboratory), Program Chair
9:00 - 10:00Formal 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:30Break
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:00Lunch
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:30Break
3:30 - 5:00Panel: Formalization and Proof of Secrecy Properties
Panel Chair: Dennis Volpano (Naval Postgraduate School)
Martín Abadi (Compaq SRC), Riccardo Focardi (U. Venezia - Ca' Foscari),
Cathy Meadows (NRL), Jon Millen (SRI)

TUESDAY June 29, 1999

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:30Break
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:00Lunch
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:30Break
3:30 - 4:30CSFW Business Meeting

WEDNESDAY June 30, 1999

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:30Break
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:00Closing remarks. Presentation of Bocce Awards