Computationally complete symbolic attacker and key exchange

We consider the problem of computational indistinguishability of protocols. We design a symbolic model, amenable to automated de-duction, such that a successful inconsistency proof implies compu-tational indistinguishability. Conversely, symbolic models of dis-tinguishability provide clues for likely computational attacks. We follow the idea we introduced earlier for reachability properties, axiomatizing what an attacker cannot violate. This results a com-putationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficul-ties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reacha-bility properties