Low-level Ideal Signatures and General Integrity Idealization

Recently we showed how to justify a Dolev-Yao type model of cryptography as used in virtually all automated protocol provers under active attacks and in arbitrary protocol environments. The justification was done by defining an ideal system handling Dolev-Yao-style terms and a cryptographic realization with the same user interface, and by showing that the realization is as secure as the ideal system in the sense of reactive simulatability. This holds the standard model of cryptography and under standard assumptions of adaptively secure primitives.

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 we tried to use as a lower layer in prior versions of the library proof. 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 justification of the Dolev-Yao type model 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.