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