Propositional Logics of Overwhelming Truth

Authors Thibaut Antoine , David Baelde



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.24.pdf
  • Filesize: 0.74 MB
  • 19 pages

Document Identifiers

Author Details

Thibaut Antoine
  • Univ Rennes, CNRS, IRISA, France
David Baelde
  • Univ Rennes, CNRS, IRISA, France

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.CSL.2025.24

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.

Subject Classification

ACM Subject Classification
  • Security and privacy → Formal methods and theory of security
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Proof theory
Keywords
  • Cryptography
  • Modal Logic
  • Sequent Calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters. Ssprove: A foundational framework for modular cryptographic proofs in coq. In CSF, pages 1-15. IEEE, 2021. URL: https://doi.org/10.1109/CSF51468.2021.00048.
  2. David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, and Solène Moreau. An interactive prover for protocol verification in the computational model. In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021, pages 537-554. IEEE, 2021. URL: https://doi.org/10.1109/SP40001.2021.00078.
  3. David Baelde, Stéphanie Delaune, Adrien Koutsos, and Solène Moreau. Cracking the stateful nut: Computational proofs of stateful security protocols using the squirrel proof assistant. In CSF, pages 289-304. IEEE, 2022. URL: https://doi.org/10.1109/CSF54842.2022.9919665.
  4. David Baelde, Caroline Fontaine, Adrien Koutsos, Guillaume Scerri, and Théo Vignon. A Probabilistic Logic for Concrete Security. In CSF 2024 - 37th IEEE Computer Security Foundations Symposium, Enschede, Netherlands, July 2024. URL: https://hal.science/hal-04577828.
  5. David Baelde, Adrien Koutsos, and Joseph Lallemand. A Higher-Order Indistinguishability Logic for Cryptographic Reasoning. In LICS'23. ACM, 2023. URL: https://inria.hal.science/hal-03981949.
  6. Gergei Bana, Rohit Chadha, and Ajay Kumar Eeralla. Formal analysis of vote privacy using computationally complete symbolic attacker. In ESORICS (2), volume 11099 of Lecture Notes in Computer Science, pages 350-372. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98989-1_18.
  7. Gergei Bana and Hubert Comon-Lundh. Towards unconditional soundness: Computationally complete symbolic attacker. In International Conference on Principles of Security and Trust, pages 189-208. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28641-4_11.
  8. Gergei Bana and Hubert Comon-Lundh. A computationally complete symbolic attacker for equivalence properties. In Gail-Joon Ahn, Moti Yung, and Ninghui Li, editors, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014, pages 609-620. ACM, 2014. URL: https://doi.org/10.1145/2660267.2660276.
  9. Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. Sok: Computer-aided cryptography. In 2021 IEEE Symposium on Security and Privacy (SP), pages 777-795, 2021. URL: https://doi.org/10.1109/SP40001.2021.00008.
  10. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In CRYPTO, volume 6841 of Lecture Notes in Computer Science, pages 71-90. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22792-9_5.
  11. David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar. Crypthol: Game-based proofs in higher-order logic. J. Cryptol., 33(2):494-566, 2020. URL: https://doi.org/10.1007/S00145-019-09341-Z.
  12. Patrick Blackburn, Maarten De Rijke, and Yde Venema. Modal logic, volume 53. Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884.
  13. Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated verification of selected equivalences for security protocols. The Journal of Logic and Algebraic Programming, 75(1):3-51, 2008. URL: https://doi.org/10.1016/J.JLAP.2007.06.002.
  14. Hubert Comon and Adrien Koutsos. Formal computational unlinkability proofs of RFID protocols. In CSF, pages 100-114. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/CSF.2017.9.
  15. Hubert Comon-Lundh, Véronique Cortier, and Guillaume Scerri. Tractable inference systems: An extension with a deducibility predicate. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 91-108. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38574-2_6.
  16. Cas Cremers, Caroline Fontaine, and Charlie Jacomme. A logic and an interactive prover for the computational post-quantum security of protocols. In SP, pages 125-141. IEEE, 2022. URL: https://doi.org/10.1109/SP46214.2022.9833800.
  17. Lorenz Demey, Barteld Kooi, and Joshua Sack. Logic and Probability. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, summer 2019 edition, 2019. URL: https://plato.stanford.edu/archives/sum2019/entries/logic-probability/.
  18. Shafi Goldwasser and Silvio Micali. Probabilistic encryption. Journal of Computer and System Sciences, 28(2):270-299, 1984. URL: https://doi.org/10.1016/0022-0000(84)90070-9.
  19. Charles L Hamblin. The modal" probably". Mind, 68(270):234-240, 1959. Google Scholar
  20. Andrzej Indrzejczak. Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus. Bulletin of the Section of Logic, 45(2), June 2016. URL: https://doi.org/10.18778/0138-0680.45.2.05.
  21. Adrien Koutsos. The 5G-AKA authentication protocol privacy. In EuroS&P, pages 464-479. IEEE, 2019. URL: https://doi.org/10.1109/EUROSP.2019.00041.
  22. Adrien Koutsos. Decidability of a sound set of inference rules for computational indistinguishability. In 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019, pages 48-61. IEEE, 2019. URL: https://doi.org/10.1109/CSF.2019.00011.
  23. Charles G. Morgan. Simple Probabilistic Semantics for Propositional K, T, B, S4, and S5. Journal of Philosophical Logic, 11(4):443-458, 1982. URL: https://www.jstor.org/stable/30226261, URL: https://doi.org/10.1007/BF00284979.
  24. Charles G. Morgan. There Is a Probabilistic Semantics for Every Extension of Classical Sentence Logic. Journal of Philosophical Logic, 11(4):431-442, 1982. URL: https://www.jstor.org/stable/30226260, URL: https://doi.org/10.1007/BF00284978.
  25. Francesca Poggiolesi. A cut-free simple sequent calculus for modal logic S5. The Review of Symbolic Logic, 1(1):3-15, 2008. URL: https://doi.org/10.1017/S1755020308080040.
  26. Guillaume Scerri and Ryan Stanley-Oakes. Analysis of key wrapping apis: Generic policies, computational security. In CSF, pages 281-295. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/CSF.2016.27.
  27. Victor Shoup. Sequences of games: a tool for taming complexity in security proofs. cryptology eprint archive, 2004. Google Scholar
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