Penn Arts & Sciences Logo

Tuesday, April 29, 2003 - 12:10pm

Paulo Mateus

Instituto Superior Técnico

Location

University of Pennsylvania

3401 Walnut, room 470

We use the probabilistic polynomial-time process calculus introduced by Lincoln, Mitchell, and Scedrov to derive compositionality properties of cryptographic protocols in the presence of computationally bounded adversaries. We focus on four types of protocols: oblivious transfer (OT), secure function evaluation, zero-knowledge proofs, and secure channel implementation. A general definition for all these cases is established following the general paradigm that a protocol is secure if it can emulate an ideal protocol. To this end, we capitalize on the semantics of the calculus and extract a Markov process of observations to set up the notion of emulation. Emulation turns out to be a congruence relation and this result leads to a general composition theorem. We derive as a corollary an associated composition result for each of the four types of protocols considered, encompassing in some cases both active and passive adversaries. As an illustration of the concepts and results in an intuitive and simple manner, we give special emphasis to the simple case of OT, incorporating an example of the protocol. Finally, we compare our approach with the approaches by R. Canetti and by B. Pfitzmann et al. This is joint work with J. Mitchell and A. Scedrov.