DIMACS Workshop on Security Analysis of Protocols

June 7 - 9, 2004
DIMACS Center, CoRE Building, Rutgers University, Piscataway, NJ

Organizers:

John Mitchell, Stanford, mitchell@cs.stanford.edu

Ran Canetti, IBM Watson, canetti@watson.ibm.com

Workshop Program:

Monday, June 7, 2004
 
 8:30 -  9:00  Registration - 1st Floor Lobby, CoRE Bldg.
               Breakfast - 4th Floor Lounge

 9:00 -  9:10  Welcome and Opening Remarks
               Mel Janowitz, Associate Director, DIMACS

 9:10 -  9:30  Welcome 
               John Mitchell, Stanford University
               Ran Canetti, IBM Watson

 9:30 - 10:30  Tutorial: Formal methods and protocol analysis
               Peter Ryan, University of Newcastle Upon Tyne

10:30 - 11:00  Break

11:00 - 12:30  Session    
 
               Modeling and Analyzing Security Protocols Using I/O Automata 
               Nancy Lynch, MIT

               Automata-based analysis of recursive cryptographic protocols
               Thomas Wilke, Kiel University

               Formal Analysis of Availability
               Carl A. Gunter, University of Pennsylvania

12:30 -  2:00  Lunch

 2:00 -  3:00  Tutorial: Towards cryptographically sound formal analysis
               Daniele Micciancio, UCSD 

 3:00 -  3:30  Break

 3:30 -  5:30  Session  

               A Reactively Secure Dolev-Yao-style Cryptographic Library
               Birgit Pfitzmann, IBM Research

               Towards Automated Computationally Faithful Verification of Cryptoprotocols
               Jan Jürjens, TU Munich

               Computational and Information-Theoretic Soundness 
               and Completeness of the Expanded Logics of Formal Encryption
               Gergei Bana, University of Pennsylvania

               Universally Composable Symbolic Analysis of Cryptographic Protocols
               Jonathan Herzog, MIT
               
 5:30          Reception - Wine and cheese - DIMACS Lounge

Tuesday, June 8, 2004

 8:30 -  9:00  Breakfast and Registration - 4th Floor CoRE Bldg.
 
 9:00 - 10:00  Tutorial - Secure Composition of Multiparty Protocols
               Yehuda Lindell, IBM Research

10:00 - 10:30  Break

10:30 - 12:30  Session   

               New Notions of Security: Achieving Universal Composability 
               without Trusted Setup
               Manoj Prabhakaran and Amit Sahai, Princeton University

               Documented Ideal Protocols: A Flexible Notion of Universal 
               Composability for Simple Protocols and no Trusted Setup
               Dominic Mayers, CalTech

               A probabilistic polynomial-time calculus for the analysis of
               cryptographic protocols
               Andre Scedrov, University of Pennsylvania

               Sequential Process Calculus and Machine Models for Simulation-based Security
               Ralf Kuesters, University of Kiel

12:30 -  2:00  Lunch

 2:00 -  3:00  Tutorial: Proving protocol properties      
               Joshua D. Guttman, MITRE

 3:00 -  3:30  Break

 3:30 -  5:30  Session     

               Machine-Checked Formalization of the Generic Model and the Random Oracle Model
               Sabrina Tarento, INRIA            

               A Notation for Multiparty Protocols of ITM's: Digging from the Tunnel's Other End
               Jesus F. Almansa, University of Aarhus
               
               Monte-Carlo Analysis of Protocols
               Radu Grosu, SUNY Stony Brook

               A Framework for Security Analysis with Team Automata
               Marinella Petrocchi, IIT-CNR, Italy

 5:30          End of Session

Wednesday, June 9, 2004 

 8:30 -  9:00  Breakfast and Registration - 4th Floor CoRE Bldg.
 
 9:00 - 10:00  Tutorial: Formal representations of polynomial-time algorithms and security
               Bruce Kapron, University of Victoria

10:00 - 10:30  Break

10:30 - 12:30  Session    

               Collusion-Free Protocols
               Silvio Micali, MIT

               A Framework for Fair (Multi-Party) Computation
               Juan Garay, Bell Labs

               Dolev-Yao-type Abstraction of Modular Exponentiation - the Cliques Case Study
               Olivier Pereira and Jean-Jacques Quisquater, UCL

               Message Equivalence and Imperfect Cryptography in a Formal Model
               Angelo Troina, Univerity of Pisa

12:30 -  1:30  Lunch

 1:30  - 2:30  Tutorial: Constraint-based methods: 
               Adding computational properties to symbolic models
               Vitaly Shmatikov, SRI

 2:30 -  3:00  Break

 3:00 -  4:30  Session  

               Towards a Hierarchy of Cryptographic Protocol Models
               Cathy Meadows, NRL

               Sound Approximations to Diffie-Hellman Using Rewrite Rules
               Christopher Lynch,  Clarkson University

               Fine-Grained MSR Specifications for Quantitative Security Analysis
               Iliano Cervesato, NRL

 4:30          End of Workshop

Previous: Participation

Next: Registration

Workshop Index

DIMACS Homepage