Protocol Indistinguishability and the Computationally Complete Symbolic Attacker

ABSTRACT. We considered the problem the computational indistinguishability of two bounded protocols. We designed a symbolic model that is amenable to automated deduction, and such that an inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. The idea is to define a computationally complete symbolic attacker in order to achieve unconditional computational soundness of the symbolic analysis. Following our previous work on reachability properties, we achieve this by axiomatizing what an attacker cannot violate. By adding computationally sound, modular axioms, a library of axioms can be built. Despite additional difficulties stemming from equivalences, the models and proofs are much simpler than in the case of reachability properties.