2 Search Results for "Bana, Gergei"

Document
DOI: 10.4230/LIPIcs.CSL.2016.34
Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4

Authors: Gergei Bana and Mitsuhiro Okada

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
In this work we look at how Fitting's embedding of first-order classical logic into first-order S4 can help in reasoning when we are interested in satisfaction "in most cases", when first-order properties are allowed to fail in cases that are considered insignificant. We extend classical semantics by combining a Kripke-style model construction of "significant" events as possible worlds with the forcing-Fitting-style semantics construction by embedding classical logic into S4. We provide various examples. Our main running example is an application to symbolic security protocol verification with complexity-theoretic guarantees. In particular, we show how Fitting's embedding emerges entirely naturally when verifying trace properties in computer security.
Cite as

Gergei Bana and Mitsuhiro Okada. Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bana_et_al:LIPIcs.CSL.2016.34,
  author =	{Bana, Gergei and Okada, Mitsuhiro},
  title =	{{Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{34:1--34:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.34},
  URN =		{urn:nbn:de:0030-drops-65746},
  doi =		{10.4230/LIPIcs.CSL.2016.34},
  annote =	{Keywords: first-order logic, possible-world semantics, Fitting embedding, asymptotic probabilities, verification of complexity-theoretic properties}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.546
Computationally Complete Symbolic Attacker in Action

Authors: Gergei Bana, Pedro Adao, and Hideki Sakurada

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{bana_et_al:LIPIcs.FSTTCS.2012.546,
  author =	{Bana, Gergei and Adao, Pedro and Sakurada, Hideki},
  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 =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.546},
  URN =		{urn:nbn:de:0030-drops-38888},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.546},
  annote =	{Keywords: Security Protocols, Symbolic Adversary, Computational Soundness}
}
  • Refine by Author
  • 2 Bana, Gergei
  • 1 Adao, Pedro
  • 1 Okada, Mitsuhiro
  • 1 Sakurada, Hideki

  • Refine by Classification

  • Refine by Keyword
  • 1 Computational Soundness
  • 1 Fitting embedding
  • 1 Security Protocols
  • 1 Symbolic Adversary
  • 1 asymptotic probabilities
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2012
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact