Abstract. 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 ...