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