DROPS

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.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.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}
}

Search Results

Documents authored by Bana, Gergei

Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4

Abstract

Cite as

Computationally Complete Symbolic Attacker in Action

Abstract

Cite as

Thanks for your feedback!

Could not send message