Welcome to the resource topic for 2012/316
Title:
Computationally Complete Symbolic Attacker in Action
Authors: Gergei Bana, Pedro Adão, Hideki Sakurada
Abstract:In this paper we show that the recent technique of computationally complete symbolic attackers proposed by Bana and Comon-Lundh for computationally sound verification is powerful enough to verify actual protocols, such as the Needham-Schroeder-Lowe Protocol. In their model, one does not define explicit Dolev-Yao adversarial capabilities but rather the limitations of the adversarial capabilities. In this paper we present a set of axioms sufficient to show that no symbolic adversary compliant with these axioms can successfully violate secrecy or authentication in case of the NSL protocol. Hence all implementations for which these axioms are sound – namely, implementations using CCA2 encryption, and satisfying a minimal parsing requirement for pairing – exclude the possibility of successful computational attacks.
ePrint: https://eprint.iacr.org/2012/316
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .