Simulation aborted because the adversary doesn't use the random oracle I'm trying to construct a proof for an encryption scheme in the Random Oracle model. This encryption scheme is like a PKE scheme but with an additional function that kind of "alters" ciphertexts without changing the underlying message using some special keys (I don't want to go into the scheme details for not diverting attention from the actual question; let's call this function "Alteration", for simplicity). In principle, the scheme is designed in such a way that in order to create valid ciphertexts, you have to use a hash function $H$ at some moment during the encryption. I later use this fact in the proof to construct the decryption oracle: assuming that $H$ is a random oracle, I use the random oracle table to extract the necessary information for answering the decryption query, and if the adversary has not used $H$, then it outputs $\perp$. The adversary cannot distinguish this behavior from a real-world execution. So far so good.

The problem I'm facing right now is with the Alteration oracle. Everything goes smoothly as long as the adversary uses the random oracle. However, the adversary may query the Alteration oracle with a ciphertext constructed without using the random oracle, but the real-world version of the Alteration function is unable to detect such situation and simply outputs the altered ciphertext correctly. In the proof, the simulator cannot respond to the query since the adversary has not used the random oracles and the simulator does not have the required special key. The thing is that I don't see that these queries are beneficial at all to the adversary: the resulting ciphertexts would also be not valid, as the original ones, so their decryption would fail. 

Therefore, in order to avoid a situation where the adversary could detect a difference between the simulation world and the real world, the only think I can think of at the moment is to abort the simulation in such situation. Of course, simply letting the proof go this way would invalidate it, since the adversary could make these problematic queries arbitrarily. I was thinking in trying something similar to the "artificial abort" technique used in the Waters IBE scheme. However, before continuing in that direction, I have the following questions.

Do proofs in the Random Oracle model generally require to handle the situation when the adversary is not using the Random Oracle (e.g., producing invalid ciphertexts)? If not, do you know any example of a scheme defined in the RO model where a similar situation occurs?
Your proof certainly has to work even if the adversary doesn't use the random oracle. One technique that you can try is to begin by proving a separate lemma that if the adversary doesn't ask a certain query first, then it definitely cannot succeed in distinguishing. Then, you proceed to prove the simulation conditioned on it asking this query.

However, if you can't prove this, then you may have to go back to the construction and change it. This reminds me of the double-encrypt-plus-NIZK way of getting CCA-secure encryption in the standard model. In that construction, the NIZK is needed since the simulator can only decrypt one of the two ciphertexts in the reduction, and cannot tell that the other is an encryption to the same. However, if it's not an encryption of the same, then in the real world this would decrypt to invalid. Nevertheless, you can't get rid of the NIZK. The simulator has to know what would happen in the real execution. Sorry for the pessimism.