A Composable Dolev-Yao-Style Cryptographic Library With Nested Operations

Michael Backes, IBM Zurich Research Lab

We present the first idealized cryptographic library that can be used like the Dolev-Yao model for automated proofs of cryptographic protocols that use nested cryptographic operations, while coming with a cryptographic implementation that is provably secure under arbitrary active attacks and arbitrary protocol environments.

Gates 4B (opposite 490) Tuesday 06/22/04 1630 hrs