License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2012.546
URN: urn:nbn:de:0030-drops-38888
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3888/
Go to the corresponding LIPIcs Volume Portal

Bana, Gergei ; Adao, Pedro ; Sakurada, Hideki

Computationally Complete Symbolic Attacker in Action

pdf-format:
49.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{bana_et_al:LIPIcs:2012:3888,
  author =	{Gergei Bana and Pedro Adao and Hideki  Sakurada},
  title =	{{Computationally Complete Symbolic Attacker  in Action}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012) },
  pages =	{546--560},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2012/3888},
  URN =		{urn:nbn:de:0030-drops-38888},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.546},
  annote =	{Keywords: Security Protocols, Symbolic Adversary, Computational Soundness}
}

Keywords: Security Protocols, Symbolic Adversary, Computational Soundness
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)
Issue Date: 2012
Date of publication: 14.12.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI