A composable cryptographic library with nested operations
Michael Backes, Birgit Pfitzmann, Michael Waidner · 2003
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.