In Dolev-Yao and other formal models, the assumptions about adversary behavior are encoded via the grammar and entailment relation, and there's no mention of a specific computational definition of encryption security.
But your question is still meaningful, and can be interpreted as follows:
If my encryption scheme is CPA secure, and my protocol is secure in the sense of Dolev-Yao, then is my protocol necessarily computationally secure?
This question has been studied, starting in a very nice paper by Abadi and Rogaway. For your question, their answer is "No, but CPA is almost enough." Caveats in the security definition involve whether the adversary can detect if two ciphertexts were generated with the same key, or if you encrypt "key cycles", whether message length is leaked, etc. The linked paper resolves all of these details.