Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-26T17:48:52.308Z Has data issue: false hasContentIssue false
  • English
  • Français

Probabilistic logic over equations and domain restrictions

Published online by Cambridge University Press:  08 March 2019

Andreia Mordido  and
Carlos Caleiro
Andreia Mordido*
Affiliation:
SQIG – Instituto de Telecomunicações, Lisbon, Portugal LASIGE, Faculdade de Ciências, Universidade de Lisboa, Portugal
Carlos Caleiro
Affiliation:
SQIG – Instituto de Telecomunicações, Lisbon, Portugal Department of Mathematics, IST – Universidade de Lisboa, Lisbon, Portugal
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We propose and study a probabilistic logic over an algebraic basis, including equations and domain restrictions. The logic combines aspects from classical logic and equational logic with an exogenous approach to quantitative probabilistic reasoning. We present a sound and weakly complete axiomatization for the logic, parameterized by an equational specification of the algebraic basis coupled with the intended domain restrictions.We show that the satisfiability problem for the logic is decidable, under the assumption that its algebraic basis is given by means of a convergent rewriting system, and, additionally, that the axiomatization of domain restrictions enjoys a suitable subterm property. For this purpose, we provide a polynomial reduction to Satisfiability Modulo Theories. As a consequence, we get that validity in the logic is also decidable. Furthermore, under the assumption that the rewriting system that defines the equational basis underlying the logic is also subterm convergent, we show that the resulting satisfiability problem is NP-complete, and thus the validity problem is coNP-complete.We test the logic with meaningful examples in information security, namely by verifying and estimating the probability of the existence of offline guessing attacks to cryptographic protocols.

Keywords

probabilistic logicequational logicsatisfiability problemofffline guessing attacks
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 29 , Issue 6 , June 2019 , pp. 872 - 895
Copyright
© Cambridge University Press 2019 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

Work done under the scope of R&D Unit 50008, financed by the applicable financial framework (FCT/MEC through national funds and when applicable co-funded by FEDER–PT2020). The first author was supported by FCT under the grant SFRH/BD/77648/2011 and by the Calouste Gulbenkian Foundation under Programa de Estímulo à Investigação 2011. The second author also acknowledges the support of EU FP7Marie Curie PIRSES-GA-2012-318986 project GeTFun: Generalizing Truth-Functionality. Work also supported by LASIGE Research Unit, ref. UID/CEC/00408/2019.

References

Abadi, M. and Cortier, V. (2005). Deciding knowledge in security protocols under (many more) equational theories. In: Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW ’ 05), IEEE, 62–76.CrossRefGoogle Scholar
Abadi, M. and Cortier, V. (2006). Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367 (1) 2–32.CrossRefGoogle Scholar
Adrian, D., Bhargavan, K., Durumeric, Z., Gaudry, P., Green, M., Halderman, J. A., Heninger, N., Springall, D., Thomé, E., Valenta, L., VanderSloot, B., Wustrow, E., Zanella-Beguelin, S. and Zimmermann, P. (2015). Imperfect forward secrecy: how Diffie-Hellman fails in practice. In: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, ACM, 5–17.Google Scholar
Baader, F. and Nipkow, T. (1999). Term Rewriting and All That, Cambridge University Press.Google Scholar
Baudet, M. (2005). Deciding security of protocols against off-line guessing attacks. In: Proceedings of 12th ACM Conference on Computer and Communications Security, 16–25, ACM.Google Scholar
Becker, B., Dax, C., Eisinger, J. and Klaedtke, F. (2007). LIRA: handling constraints of linear arithmetics over the integers and the reals. In: International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 4590, Springer, 307–310.CrossRefGoogle Scholar
Beurdouche, B., Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P. Y. and Zinzindohoue, J. K. (2015). A messy state of the union: taming the composite state machines of TLS. In: Symposium on Security and Privacy 2015, IEEE, 535–552.CrossRefGoogle Scholar
Caleiro, C., Casal, F. and Mordido, A. (2016). DNFSAT-DEqPrL solver. Available online at https://github.com/fcasal/satdeqprl.git.Google Scholar
Caleiro, C., Casal, F. and Mordido, A. (2017a). Classical generalized probabilistic satisfiability. Proceedings of the 26th International Joint Conference on Artificial Intelligence, AAAI Press, 908–914.Google Scholar
Caleiro, C., Casal, F. and Mordido, A. (2017b). Generalized probabilistic satisfiability. Electronic Notes in Theoretical Computer Science 332 39–56.CrossRefGoogle Scholar
Conchinha, B., Basin, D. and Caleiro, C. (2010). Efficient decision procedures for message deducibility and static equivalence. In: Proceedings of 7th International Workshop on Formal Aspects in Security and Trust, LNCS, vol. 6561, Springer, 34–49.CrossRefGoogle Scholar
Conchinha, B., Basin, D. and Caleiro, C. (2013). Symbolic probabilistic analysis of off-line guessing. In: European Symposium on Research in Computer Security, Lecture Notes in Computer Science, vol. 8134, Springer, 363–380.Google Scholar
Corin, R. J. and Etalle, S. (2004). A simple procedure for finding guessing attacks. Centre for Telematics and Information Technology, University of Twente.Google Scholar
Cortier, V., Kremer, S. and Warinschi, B. (2011). A survey of symbolic methods in computational analysis of cryptographic systems. Journal of Automated Reasoning 46 (3–4) 225–259.CrossRefGoogle Scholar
Dershowitz, N., Okada, M. and Sivakumar, G. (1988). Canonical conditional rewrite systems. In: Proceedings of the 9th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 310, Springer, 538–549.CrossRefGoogle Scholar
Dolev, D. and Yao, A. (1983). On the security of public key protocols. IEEE Transactions on Information Theory 29 (2) 198–208.CrossRefGoogle Scholar
Fagin, R., Halpern, J. Y. and Megiddo, N. (1990). A logic for reasoning about probabilities. Information and Computation 87 (1) 78–128.CrossRefGoogle Scholar
Finger, M. and De Bona, G. (2011). Probabilistic satisfiability: Logic-based algorithms and phase transition, IJCAI, 528–533.Google Scholar
Gong, L., Lomas, M. A., Needham, R. M. and Saltzer, J.H. (1993). Protecting poorly chosen secrets from guessing attacks. Journal on Selected Areas in Communications 11 (5) 648–656.CrossRefGoogle Scholar
Henkin, L. (1949). The completeness of the first-order functional calculus. The Journal of Symbolic Logic 14 (03) 159–166.CrossRefGoogle Scholar
Montalto, B. and Caleiro, C. (2009). Modeling and reasoning about an attacker with cryptanalytical capabilities. Electronic Notes in Theoretical Computer Science 253 (3) 143–165.CrossRefGoogle Scholar
Mateus, P., Sernadas, A. and Sernadas, C. (2005). Exogenous semantics approach to enriching logics. Essays on the Foundations of Mathematics and Logic 1 165–194.Google Scholar
Mordido, A. (2017). A Probabilistic Logic Over Equations and Domain Restrictions. Phd thesis, IST, Universidade de Lisboa.Google Scholar
Mordido, A. and Caleiro, C. (2015). An equation-based classical logic. In: Proceedings of the 22nd InternationalWorkshop on Logic, Language, Information, and Computation, Lecture Notes in Computer Science, vol. 9160, Springer, 38–52.CrossRefGoogle Scholar
Nieuwenhuis, R., Oliveras, A. and Tinelli, C. (2006). Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL (T). Journal of the ACM 53 (6) 937–977.CrossRefGoogle Scholar
Pearl, J. (1987). Do We Need Higher-Order Probabilities and, If So, What Do They Mean? UCLA, Computer Science Department.Google Scholar
Shoenfield, J. R. (2010). Mathematical logic, AK Peters/CRC Press.Google Scholar
Van Eijck, J. and Schwarzentruber, F. (2014). Epistemic probability logic simplified. Advances in Modal Logic 10 158–177.Google Scholar