I've a problem with a protocol for which I can prove the security if the messages sent by the adversary are sent in clear, but I can't prove the security anymore if the messages sent by the adversary are encrypted... and this is a bit strange since I expect the protocol to also be secure in that second case.

More precisely, I'm considering a protocol for which a server Bob receives a message $k$ from Alice (this can be seen as an encryption of a bit string $d_0$ under the secret public key $t_k$) and sends back a message $y$ (which can also be seen as an encryption of some messages $x$ under the same public key $k$ of Alice: not that due to the shape of the protocol I really need to use this exact same key). In the security proof, I'd like to show that no malicious Bob can find a secret value $\theta_\pi=f(x,d_0)$ that should look random otherwise.

The good news is that if I know $x$, I can invert $f$ and find $d_0$. Therefore if a malicious Bob knows $x$, I could do a reduction to prove that if Bob can find $\theta_\pi$ they Bob also knows $d_0 = f^{-1}(x,\theta_\pi)$: this is a contradiction since the encryption is IND-CPA secure.

Unfortunately, this reduction does not work because the malicious Bob may not "know" $x$: they only send an encrypted version $y$ of it: and during the reduction I can't decrypt this $y$ since the key is only known to Alice (this is unavoidable in my case)...

Is there some methods to still prove security in that case? I guess I need something like semantic security but where the function that is computed is not efficiently computable (this is already the case in the current definition) and also depends on some outputs of the adversary.

I've a problem with a protocol for which I can prove the security if the messages sent by the adversary are sent in clear, but I can't prove the security anymore if the messages sent by the adversary are encrypted... and this is a bit strange since I expect the protocol to also be secure in that second case.

More precisely, I'm considering a protocol for which a server Bob receives a message $k$ from Alice (this can be seen as an encryption of a bit string $d_0$ under the secret public key $t_k$) and sends back a message $y$ (which can also be seen as an encryption of some messages $x$ under the same public key $k$ of Alice: not that due to the shape of the protocol I really need to use this exact same key). In the security proof, I'd like to show that no malicious Bob can find a secret value $\theta_\pi=f(x,d_0)$ that should look random otherwise.

The good news is that if I know $x$, I can invert $f$ and find $d_0$. Therefore if a malicious Bob knows $x$, I could do a reduction to prove that if Bob can find $\theta_\pi$ they Bob also knows $d_0 = f^{-1}(x,\theta_\pi)$: this is a contradiction since the encryption is IND-CPA secure.

Unfortunately, this reduction does not work because the malicious Bob may not "know" $x$: they only send an encrypted version $y$ of it: and during the reduction I can't decrypt this $y$ since the key is only known to Alice (this is unavoidable in my case)...

Is there some methods to still prove security in that case? I guess I need something like semantic security but where the function that is computed is not efficiently computable (this is already the case in the current definition) and also depends on some outputs of the adversary.

EDIT

To answer to Mikero, I think that in your argument we need to say something like that:

If we manage to get the right box, then I agree that the proof follows easily. But I'm not sure how to prove the equivalence between these two scenarios. I don't think this is a direct reduction to IND-CPA security, because the distinguisher also has access to $\theta_\pi$ which is linked with some information about a decoding of $y$. I guess it would also be nice to show that the first diagram is equivalent to

but not sure how to prove that (of course $Ideal Func_1$ is distinguishable from $Ideal Func_3$, the question is when we add the simulator on top).