Program
DIMACS Workshop on Design and Formal Verification of Security Protocols
September 3 - 5, 1997
DIMACS Center, CoRE Building, Rutgers University, Piscataway, NJ



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 Inn
4701 Stelton Road
Piscataway, NJ
732-753 5500

September 3, 1997

Techniques and Models 8:30 - 8:45 Welcome 8:45 - 10:30 Panel 1: Model Checkers W. Marrero, E. Clarke, S. Jha, Carnegie Mellon University A Model Checker for Authentication Protocols Z. Dang, R.A.Kemmerer, University of California at Santa Barbara Using the ASTRAL Model Checker for Cryptographic Protocol Analysis T. Kozlowski, S.A. Smolka, SUNY at Stonybrook Digital Signatures With Encryption: Fact and Fiction M. Debbabi, M. Mejri, N. Tawbi, I. Yahmadi, Laval University A New Algorithm for the Automatic Verification of Authentication Protocols: From Specifications to Flaws and Attack Scenarios 11:00 - 12:30 Panel2: Theorem Provers J. Bryans, S.Scheider, Royal Holloway and Bedford New College CSP, PVS, and a Recursive Authentication Protocol P. Abdulla, B.Jonsson, A.Nylen, University of Uppsala Modeling and Automated Verification of Authentication Protocols B. De Decker, F. Piessens, Katholieke Universiteit Leuven Cryptolog: A Theorem Prover for Cryptographic Protocols J. Alvess-foss, T. Soule, University of Idaho A Weakest Precondition Calculus for Analysis of Cryptographic Protocols 12:30 - 1:30 Lunch 1:30 - 3:30 Panel 3: Formal Models A.W. Roscoe, M.H. Goldsmith, Oxford University Computing Laboratory and Formal Systems (Europe) Ltd The Perfect ``Spy'' for Model-Checking Cryptoprotocols C. Boyd, Queensland University of Technology Extensional Goals in Authentication Protocols R. Focardi, A. Ghelli, R. Gorrieri, Universita' Ca' Foscari di Venezia and Universita' di Bologna Using Non Interference for the Analysis of Security Protocols A. Maneki, NSA An Application of the WDL Theory of System Composition to the Analysis of Cryptographic Protocols C.A. Gunter, T. Jim, University of Pennsylvania Design of an Application-Level Security Infrastructure 4:00 - 5:30 Panel 4: Belief Logics and their Combination with Other Techniques A. Bleeker, L. Meertens, CWI, Amsterdam A Semantics for BAN Logic A. Huima, T. Aura, Helsinki University of Technology Using a Multimodal Logic to Express Conflicting Interests in Security Protocols J.P. Beckmann, P. de Goede, A. Hutchison, University of Cape Town SPEAR: Security Protocol Engineering and Analysis Resources D. Kindred, J. Wing, Carnegie Mellon University Closing the Idealization Gap with Theory Generation 7:00 Dinner at Holiday Day Inn

September 4, 1997

Applications 9:00 - 10:30 Panel 5: Panel on Analysis and Implementation of Secure Electronic Mail Protocols chair : M. Stillman panelists : D. Rosenthal, ORA S.K. Chin, Syracuse University M. Barjaktarovic, Wilkes University 11:00 - 12:30 Panel 6: Real Protocols S. Brackin, Arca Systems Automatic Formal Analysis of Two Large Commercial Protocols S. Mocas and T. Schubert, Portland State University Formal Analysis of IP Layer Security J. Mitchell, V. Shmatikov, U. Stern, Stanford University Finite-State Analysis of SSL 3.0 and related Protocols F. Germeau and G. Leduc, Universite de Liege Model-based Design and Verification of Security Protocols using LOTOS G. Bella and L. C. Paulson, Cambridge University Using Isabelle to Prove Properties of the Kerberos Authentication System 12:30 - 1:30 Lunch 1:30 - 3:30 Panel 7: What Designers Need From Formal Methods chair : C. Meadows, NRL panelists : S. Kent, BBN C. Ellison, Cybercash J. Brainard, RSA Laboratories R. Cordery, Pitney Bowes 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? chair : Y. Desmedt, U. of Wisconsin-Milwaukee panelists : M. Burmester, Royal Holloway and Bedford New College J. Millen, MITRE others TBA 11:00 - 12:30 Panel 9: High Fidelity A. Gillet, M. Joye, J.-J. Quisquater, University of Louvain Cautionary Note for Protocol Designers: Security Proof is not Enough S. Stubblebine and C. Meadows, AT&T and NRL On Known and Chosen Cipher Pairs T. Markham, Secure Computing Cryptographic Module Flaws and Analysis Techniques C. Gunter, I. Lee, A. Scedrov, University of Pennsylvania Two Weak Links in the Formal Methods Chain

Previous: Participation
Next: Registration
Workshop Index
DIMACS Homepage
Contacting the Center
Document last modified on February 28, 1997.