DIMACS Workshop on
Design and Formal Verification of Security Protocols

There will be a reception on Tuesday-September 2, 1997, at 7:00 pm, and dinner on Wednesday, September 3, 1997, at 7:00 pm at:

Holiday Day Inn

4701 Stelton Road

Piscataway, NJ

732-753 5500

for participants of this workshop.

September 3, 1997

Techniques and Models

8:30 - 8:45 Welcome

8:45 - 10:30 Panel 1: Model Checkers, Chair: Gavin Lowe

A Model Checker for Authentication Protocols [HTML]: W. Marrero, E. Clarke, S. Jha, Carnegie Mellon University
Using the ASTRAL Model Checker for Cryptographic Protocol Analysis [HTML]: Z. Dang, R.A.Kemmerer, University of California at Santa Barbara
Digital Signatures With Encryption: Fact and Fiction (Extended Abstract) [HTML]: T. Kozlowski, S.A. Smolka, SUNY at Stonybrook
Modelling and Analysis of Security Protocols: I. Zakiuddin, DRA

11:00 - 12:30 Panel 2: Theorem Provers, Chair: Dick Kemmerer

CSP, PVS, and a Recursive Authentication Protocol [HTML]: J. Bryans, S.Scheider, Royal Holloway and Bedford New College
Modeling and Automated Verification of Authentication Protocols [HTML]: P. Abdulla, B.Jonsson, A.Nylen, University of Uppsala
CryptoLog: A Theorem Prover for Cryptographic Protocols [HTML]: B. De Decker, F. Piessens, Katholieke Universiteit Leuven
A Weakest Precondition Calculus for Analysis of Cryptographic Protocols [HTML]: J. Alves-Foss, T. Soule, University of Idaho

12:30 - 1:30 Lunch

1:30 - 3:30 Panel 3: Formal Models, Chair: Paul Syverson

The Perfect ``Spy'' for Model-Checking Cryptoprotocols [HTML]: A.W. Roscoe, M.H. Goldsmith, Oxford University Computing Laboratory and Formal Systems (Europe) Ltd.
Extensional Goals in Authentication Protocols [HTML]: C. Boyd, Queensland University of Technology
Using Non Interference for the Analysis of Security Protocols [HTML]: R. Focardi, Universita Ca' Foscari di Venezia; A. Ghelli, R. Gorrieri, Universita di Bologna
An Application of the WDL Theory of System Composition to the Analysis of Cryptographic Protocols: A. Maneki , NSA
Design of an Application-Level Security Infrastructure [HTML]: C.A. Gunter, T. Jim, University of Pennsylvania

4:00 - 5:30 Panel 4: Combining Belief Logics with Other Techniques, Chair: Stuart Stubblebine

A Semantics for BAN Logic [HTML]: A. Bleeker, L. Meertens, CWI, Amsterdam
Using a Multimodal Logic to Express Conflicting Interests in Security Protocols [HTML]: A. Huima, T. Aura, Helsinki University of Technology
SPEAR: Security Protocol Engineering and Analysis Resources [HTML]: J.P. Beckmann, P. de Goede, A. Hutchison, University of Cape Town
Closing the Idealization Gap with Theory Generation (Extended Abstract) [HTML]: D. Kindred, J. Wing, Carnegie Mellon University

7:00 Dinner at Holiday Day Inn

Applications

9:00 - 10:30 Panel 5: Panel on Analysis and Implementation of Secure Electronic Mail Protocols

Chair:: M. Stillman [PostScript] [HTML]
Panelists:: D. Rosenthal, ORA
S.K. Chin, Syracuse University
M. Barjaktarovic, Wilkes University

11:00 - 12:30 Panel 6: Real Protocols, Chair: Hilarie Orman

Automatic Formal Analysis of Two Large Commercial Protocols [HTML]: S. Brackin, Arca Systems
Formal Analysis of IP Layer Security [HTML]: S. Mocas and T. Schubert, Portland State University
Finite-State Analysis of SSL 3.0 and Related Protocols [HTML]: J. Mitchell, V. Shmatikov, U. Stern, Stanford University
Model-based Design and Verification of Security Protocols using LOTOS [HTML]: F. Germeau and G. Leduc, Universite de Liege
Using Isabelle to Prove Properties of the Kerberos Authentication System [HTML]: G. Bella and L. C. Paulson,Cambridge University

12:30 - 1:30 Lunch

1:30 - 3:30 Panel 7: What Designers Need From Formal Methods

Chair :: C. Meadows, NRL [PostScript] [HTML]
Panelists:: S. Kent, BBN
C. Ellison, Cybercash
J. Brainard, RSA Laboratories
R. Cordery, Pitney Bowes [PostScript] [HTML]

3:30 - 5:30 Demos

Issues and New Directions

9:00 - 10:30 Panel 8: Design vs. Verification: Is Verification the Wrong Approach?

Chair:: Y. Desmedt, University of Wisconsin-Milwaukee [PostScript] [HTML]
Panelists:: M. Burmester, Royal Holloway and Bedford New College [PostScript] [HTML]
J. Millen, The MITRE Corporation [PostScript] [HTML]

11:00 - 12:30 Panel 9: High Fidelity, Chair: Virgil Gligor

Cautionary Note for Protocol Designers: Security Proof is not Enough [HTML]: A. Gillet, M. Joye, J.-J. Quisquater, University of Louvain
On Known and Chosen Cipher Pairs [HTML]: S. Stubblebine and C.A. Meadows, AT&T Labs-Research and Naval Research Laboratory
Two Weak Links in the Formal Methods Chain [HTML]: C. Gunter, I. Lee, A. Scedrov, University of Pennsylvania
A New Algorithm for the Automatic Verification of Authentication Protocols: From Specifications to Flaws and Attack Scenarios [HTML]: M. Debbabi, M. Mejri, N. Tawbi, I. Yahmadi, Laval University