3 Search Results for "Bana, Gergei"

Document
DOI: 10.4230/LIPIcs.CSL.2025.24
Propositional Logics of Overwhelming Truth

Authors: Thibaut Antoine and David Baelde

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Cryptographers consider that asymptotic security holds when, for any possible attacker running in polynomial time, the probability that the attack succeeds is negligible, i.e. that it tends fast enough to zero with the size of secrets. In order to reason formally about cryptographic truth, one may thus consider logics where a formula is satisfied when it is true with overwhelming probability, i.e. a probability that tends fast enough to one with the size of secrets. In such logics it is not always the case that either ϕ or ⌝ϕ is satisfied by a given model. However, security analyses will inevitably involve specific formulas, which we call determined, satisfying this property - typically because they are not probabilistic. The Squirrel proof assistant, which implements a logic of overwhelming truth, features ad-hoc proof rules for this purpose. In this paper, we study several propositional logics whose semantics rely on overwhelming truth. We first consider a modal logic of overwhelming truth, and show that it coincides with S5. In addition to providing an axiomatization, this brings a well-behaved proof system for our logic in the form of Poggiolesi’s hypersequent calculus. Further, we show that this system can be adapted to elegantly incorporate reasoning on determined atoms. We then consider a logic that is closer to Squirrel’s language, where the overwhelming truth modality cannot be nested. In that case, we show that a simple proof system, based on regular sequents, is sound and complete. This result justifies the core of Squirrel’s proof system.
Cite as

Thibaut Antoine and David Baelde. Propositional Logics of Overwhelming Truth. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{antoine_et_al:LIPIcs.CSL.2025.24,
  author =	{Antoine, Thibaut and Baelde, David},
  title =	{{Propositional Logics of Overwhelming Truth}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.24},
  URN =		{urn:nbn:de:0030-drops-227818},
  doi =		{10.4230/LIPIcs.CSL.2025.24},
  annote =	{Keywords: Cryptography, Modal Logic, Sequent Calculus}
}
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}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2016
  • 1 2012

  • Refine by Author
  • 2 Bana, Gergei
  • 1 Adao, Pedro
  • 1 Antoine, Thibaut
  • 1 Baelde, David
  • 1 Okada, Mitsuhiro
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 1 Security and privacy → Formal methods and theory of security
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 1 Computational Soundness
  • 1 Cryptography
  • 1 Fitting embedding
  • 1 Modal Logic
  • 1 Security Protocols
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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