in Proceedings of 10th ACM Conference on Computer and Communications Security (CCS), pp. 220-230, October 2003. Preprint on IACR ePrint 2003/015.
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 active attacks.
This publication is accompanied by links to downloadable versions of this publication. These documents do not necessarily correspond exactly to the cited version. Instead, in most cases full or updated versions are provided. For access to the official version, follow the "Official version" link to the publishers site.