Computationally Complete Symbolic Attacker in Action

Abstract : We show that the recent technique of computationally complete symbolic attackers proposed by Bana and Comon-Lundh [6] for computationally sound verification of security protocols is powerful enough to verify actual protocols. In their work, Bana and Comon-Lundh presented only the general framework, but they did not introduce sufficiently many axioms to actually prove protocols. We present a set of axioms—some generic axioms that are computationally sound for all PPT algorithms, two specific axioms that are sound for CCA2 secure encryptions, and a further minimal parsing assumption for pairing—and illustrate the power of this technique by giving the first computationally sound verification (secrecy and authentication) via symbolic attackers of the NSL Protocol that does not need any further restrictive assumptions about the computational implementation. In other words, all implementations for which the axioms are sound—namely, implementations using CCA2 encryption, and satisfying the parsing requirement for pairing—exclude the possibility of successful computational attacks. Furthermore, the axioms are entirely modular and not particular to the NSL protocol (except for the parsing assumption without which there is an attack).
Type de document :
Communication dans un congrès
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), 2012, Unknown, Afghanistan. 2012, Leibniz International Proceedings in Informatics (LIPIcs)
Liste complète des métadonnées

https://hal.inria.fr/hal-00863379
Contributeur : Ben Smyth <>
Soumis le : mercredi 18 septembre 2013 - 17:37:28
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

  • HAL Id : hal-00863379, version 1

Collections

Citation

Gergei Bana, Pedro Ad Ao, Hideki Sakurada. Computationally Complete Symbolic Attacker in Action. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), 2012, Unknown, Afghanistan. 2012, Leibniz International Proceedings in Informatics (LIPIcs). 〈hal-00863379〉

Partager

Métriques

Consultations de la notice

79