LIPIcs.FSTTCS.2012.546.pdf
- Filesize: 0.53 MB
- 15 pages
Document
Computationally Complete Symbolic Attacker in Action
Authors
-
Part of:
Volume:
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2012-12-14
Cite As Get BibTex
Gergei Bana, Pedro Adao, and Hideki Sakurada. Computationally Complete Symbolic Attacker in Action. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 546-560, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
https://doi.org/10.4230/LIPIcs.FSTTCS.2012.546
Abstract
We show that the recent technique of computationally complete symbolic attackers proposed by Bana and Comon-Lundh [POST 2012] 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, and two specific axioms that are sound for CCA2 secure encryptions -- 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. The axioms are entirely modular, not particular to the NSL protocol.
Subject Classification
Keywords
- Security Protocols
- Symbolic Adversary
- Computational Soundness
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads