Automated tools such as model checkers and theorem provers for the analysis of security protocols typically abstract from cryptography by Dolev-Yao models, i.e., they replace real cryptographic operations by term algebras. The soundness of Dolev-Yao models with respect to real cryptographic security definitions has received significant attention in the last years. Until recently, all published results were positive, i.e., they show that various classes of Dolev-Yao models are indeed sound with respect to various soundness definitions. Here we discuss impossibility results. In particular, we present such results for Dolev-Yao models with hash functions, and for the strong security notion of blackbox reactive simulatability (BRSIM)/UC. We show that the impossibility even holds if no secrecy (only collision resistance) is required of the Dolev-Yao model of the hash function, or if probabilistic hashing is used, or certain plausible protocol restrictions are made. We also survey related results for XOR. In addition, we start to make some impossibility results explicit that tacitly underly prior soundness results in the sense of motivating unusual choices in the Dolev-Yao models or the realizations. We also start to discuss which of the problems known for BRSIM/UC soundness extend to weaker soundness notions.