Title:	Sound cryptographic abstractions for automated proofs

Speaker: Birgit Pfitzmann, IBM Zurich

Place: 	32-G449, Patil/Kiva, Stata Center, 32 Vassar St.
Time: 	10:30 am - noon
Date: 	Friday, September 22, 2006

Abstract:

Security-critical systems are an important application area for formal methods. However, such systems often 
contain cryptographic subsystems. The natural definitions of these subsystems are probabilistic and in most cases 
computational. Hence it is not obvious how one can treat cryptographic subsystems in a sound way within formal 
methods, in particular if one does not want to encumber the proof of an overall system by probabilities and 
computational restrictions due only to its cryptographic subsystems.

We survey our progress on integrating cryptography into formal models, in particular our work on reactive 
simulatability (RSIM), a refinement notion suitable for cryptography. We also present the underlying system model 
which unifies a computational and a more abstract presentation and allows generic distributed scheduling. We show 
the relation of RSIM and other types of specifications.

In particular, we present soundness results as well as impossibility results for the classical abstractions of 
cryptography used in the formal-methods community, the abstraction by initial models of term algebras, also 
called Dolev-Yao models or symbolic cryptography.