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

September 4, 1997

9:00 - 10:30 Panel 5: Panel on Analysis and Implementation of Secure Electronic Mail Protocols
M. Stillman [PostScript]  [HTML]
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]
S. Kent, BBN
C. Ellison, Cybercash
J. Brainard, RSA Laboratories
R. Cordery, Pitney Bowes [PostScript]  [HTML]

3:30 - 5:30 Demos

September 5, 1997

Issues and New Directions
9:00 - 10:30 Panel 8: Design vs. Verification: Is Verification the Wrong Approach?
Y. Desmedt, University of Wisconsin-Milwaukee [PostScript]  [HTML]
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