[FOM] DIMACS Workshop on Security Analysis of Protocols

[Andre Scedrov]

           DIMACS Workshop on Security Analysis of Protocols
                          June 7 - 9, 2004
     DIMACS Center, CoRE Building, Rutgers University, Piscataway, NJ

Organizers: 
John Mitchell, Stanford, mitchell at cs.stanford.edu 
Ran Canetti, IBM Watson, canetti at watson.ibm.com 

Presented under the auspices of the Special Focus on Communication Security 
and Information Privacy. 

http://dimacs.rutgers.edu/Workshops/Protocols/

The analysis of cryptographic protocols is a fundamental and challenging area 
of network security research. Traditionally, there have been two main 
approaches. One is the logic approach aimed at developing automated tools for 
the formal verification of protocols. The other is the computational or 
complexity-theoretic approach that characterizes protocol security as a set of
computational tasks and proves protocol security via reduction to the strength
of the underlying cryptographic functions. Although these two lines of work 
share a common goal, there has been little commonality between them until the 
last year or two. 

The goal of this workshop is to promote work on security analysis of protocols
and provide a forum for cooperative research combining the logical and 
complexity-based approaches. 

The workshop will include tutorials on the basics of each approach and will 
allow researchers from both communities to talk about their current work. 


------------------------
Tentative Schedule
------------------------

Monday June 7

9:00  Welcome 
9:30  Tutorial   Peter Ryan: Formal methods and protocol analysis
10:30 Break
11:00 Session    

Nancy Lynch:
Modeling security protocols using I/O automata

Thomas Wilke:
Automata-based analysis of recursive cryptographic protocols

Carl A. Gunter
Formal Analysis of Availability

12:30 Lunch

2:00 Tutorial   Daniele Micciancio: Towards cryptographically sound
formal 
                analysis 
3:00 Break
3:30 Session  

Birgit Pfitzmann:
A Reactively Secure Dolev-Yao-style Cryptographic Library

Jan Jürjens:
Automated Computationally Faithful Verification of Cryptoprotocols:
Applying and Extending the Abadi-Rogaway-Jürjens Approach

Jonathan Herzog:
Universally Composable Symbolic Analysis of Cryptographic Protocols

5:00 Reception   Wine and cheeese at DIMACS

Tuesday  June 8  

 9:30 Tutorial   Yehuda Lindell: On composability of cryptographic
protocols
10:30 Break
11:00 Session   

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

Dominic Mayers:
Universal Composability With Priced Ideal Protocols

Andre Scedrov:
A probabilistic polynomial-time calculus for the analysis of
cryptographic protocols


12:30 Lunch

2:00 Tutorial     Joshua D. Guttman: Proving protocol properties 
3:00 Break
3:30 Session     

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

M. Petrocchi:
A Framework for Security Analysis with Team Automata

Ralf Kuesters:
Sequential Process Calculus and Machine Models for Simulation-based
Security

Gergely Bana:
Computational and Information-Theoretic Soundness 
and Completeness of the Expanded Logics of Formal Encryption

5:30 End of session


19:30 Banquet dinner  (location TBA)

Wednesday June 9

9:30 Tutorial: Bruce Kapron: Formal representions of polynomial-time 
               algorithms and security

10:30 Break
11:00 Session    

Silvio Micali:
Collusion-Free Protocols

Juan Garay:
A Framework for Fair (Multi-Party) Computation

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


12:30 Lunch

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

2:30 Break
2:45 Session  

Cathy Meadows:
Towards a Hierarchy of Cryptographic Protocol Model

Angelo Trolina:
Message Equivalent and Imperfect Cryptography in a Formal Model

Christopher Lynch:
Sound Approximations to Diffie-Hellman Using Rewrite Rules

Iliano Cervesato:
Fine-Grained MSR Specifications for Quantitative Security Analysis

4:45 End

=============================================================================