Towards Unconditional Soundness: Computationally Complete Symbolic Attacker
The authors consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. They neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. They propose in this paper a different approach: everything is possible in the symbolic model, unless it contradicts a computational assumption. In this way, they obtain unconditional soundness almost by construction. And they do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works.