Computationally Complete Symbolic Attacker in Action

International audienceWe show that the recent technique of computationally complete symbolic attackersproposed by Bana and Comon-Lundh [6] for computationally sound verification of securityprotocols is powerful enough to verify actual protocols. In their work, Bana and Comon-Lundhpresented only the general framework, but they did not introduce sufficiently many axioms toactually prove protocols.We present a set of axioms—some generic axioms that are computationally sound for all PPTalgorithms, two specific axioms that are sound for CCA2 secure encryptions, and a further minimalparsing assumption for pairing—and illustrate the power of this technique by giving thefirst computationally sound verification (secrecy and authentication) via symbolic attackers ofthe NSL Protocol that does not need any further restrictive assumptions about the computationalimplementation.In other words, all implementations for which the axioms are sound—namely, implementationsusing CCA2 encryption, and satisfying the parsing requirement for pairing—exclude the possibilityof successful computational attacks. Furthermore, the axioms are entirely modular andnot particular to the NSL protocol (except for the parsing assumption without which there is anattack)