Tag Info

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 ...

This question has been studied, starting in a very nice paper by Abadi and Rogaway. [...] The linked paper resolves all of these details. Please be aware that the paper by Abadi and Rogaway cited by another answer here only considers the passive adversary case, i.e., an adversary that can only eavesdrop but not insert messages. The active adversary ...