Key substitution in the symbolic analysis of cryptographic protocols

Key substitution vulnerable signature schemes are signature schemes that permit an intruder, given a public verification key and a signed message, to compute a pair of signature and verification keys such that the message appears to be signed with the new signature key. Schemes vulnerable to this attack thus permit an active intruder to claim to be the issuer of a signed message. In this paper, we investigate and solve positively the problem of the decidability of symbolic cryptographic protocol analysis when the signature schemes employed in the concrete realisation have this property.