What are the cryptographic assumptions in the Dolev Yao model? In the Dolev Yao model for interactive protocols, the cryptographic primitive (encryption, for example) is considered as a blackbox.

Does blackbox here mean that the primitive is to be considered CPA secure, or does it even require CCA security?

My guess is that CPA is sufficient (and it is the minimum requirement), since the adversary model is rather passive. But could someone confirm this?
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.