Paper 2012/316

Computationally Complete Symbolic Attacker in Action

Gergei Bana, Pedro Adão, and 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.

Note: Simplified the soundness proofs and changed the title

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Unknown where it was published
Keywords
symbolic verificationcomputational soundness
Contact author(s)
bana @ math upenn edu
History
2012-10-29: last of 6 revisions
2012-06-05: received
See all versions
Short URL
https://ia.cr/2012/316
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2012/316,
      author = {Gergei Bana and Pedro Adão and Hideki Sakurada},
      title = {Computationally Complete Symbolic Attacker in Action},
      howpublished = {Cryptology ePrint Archive, Paper 2012/316},
      year = {2012},
      note = {\url{https://eprint.iacr.org/2012/316}},
      url = {https://eprint.iacr.org/2012/316}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.