Low-level Ideal Signatures and General Integrity Idealization

Recently Backes, Pfitzmann and Waidner solved the long-standing open problem of justifying a Dolev-Yao type model of cryptography as used in virtually all automated protocol provers. They define a flexible toolbox for constructing abstract nested cryptographic terms and for using them in arbitrary protocols, together with a cryptographic realization provably secure under arbitrary active attacks in the standard model of cryptography. While treating a term algebra is the point of that paper, a natural question is whether the proof could be more modular, e.g., by using a low-level idealization of signature schemes similar to the treatment of encryption. We present a low-level ideal signature system that could be used as a lower layer in this toolbox. It may be of independent interest for cryptography because idealizing signature schemes has proved surprisingly error-prone. However, we also explain why using it makes the overall proof of the toolbox more complicated instead of simpler. We further present a technique, integrity idealization, for mechanically constructing composable low-level ideal systems for other cryptographic primitives that have "normal" cryptographic integrity definitions.

A condensed version of this report has appeared in: Proc. 7th Information Security Conf. "ISC 2004,"Palo Alto, CA, Lecture Notes in Computer Science, Vol. 3225, K. Zhang, Y. Zheng (Eds.) (Springer, Berlin, 2004), pp. 39-51