Abstract
In the formal study of security protocols and access control systems, fragments of intuitionistic logic play a vital role. These are required to be efficient, and are typically disjunction-free. In this paper, we study the complexity of adding disjunction to these subsystems. Our lower bound results show that very little needs to be added to disjunction to get co-NP-hardness, while our upper bound results show that even a system with conjunction, disjunction, and restricted forms of negation and implication is in co-NP. Our upper bound proofs also suggest parameters which we can bound to obtain PTIME algorithms.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
From now on, whenever we refer to the complexity of a logic, we implicitly mean the complexity of the derivability problem for it.
- 2.
It is important to note that we consider only the negation elimination rule. The algorithms in this section do not work in the presence of the \(\lnot {i}\) rule. Nor do we know of a straightforward modification to handle the \(\lnot {i}\) rule. It is not easy to say without further study whether the complexity stays the same or increases, either.
References
Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM TOPLAS 15(4), 706–734 (1993)
Baskar, A., Naldurg, P., Raghavendra, K.R., Suresh, S.P.: Primal infon logic: derivability in polynomial time. In: FSTTCS 2013, LIPIcs, vol. 24, pp. 163–174 (2013)
Baskar, A., Ramanujam, R., Suresh, S.P.: A DEXPTIME-complete Dolev-Yao theory with distributive encryption. In: Hlinený, P., Kucera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 102–113. Springer, Heidelberg (2010)
Beklemishev, L.D., Gurevich, Y.: Propositional primal logic with disjunction. J. Log. Comp. 24(1), 257–282 (2014)
Chagrov, A., Zakharyaschev, M.: Modal Logic. Clarendon Press, Oxford (1997)
Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decisions in presence of exclusive or. In: LICS 2003, pp. 271–280 (2003)
Comon-Lundh, H., Treinen, R.: Easy intruder deductions. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 225–242. Springer, Heidelberg (2003)
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29, 198–208 (1983)
Gabbay, D.M., de Jongh, D.H.J.: A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property. J. Sym. Log. 39(1), 67–78 (1974)
Gurevich, Y., Neeman, I.: DKAL: Distributed-knowledge authorization language. In: 21st IEEE CSF Symposium, pp. 149–162. IEEE Press, New York (2008)
Gurevich, Y., Neeman, I.: Logic of infons: the propositional case. ACM Trans. Comp. Log. 12(2), 9:1–9:28 (2011)
Kurokawa, H.: Hypersequent calculi for intuitionistic logic with classical atoms. APAL 161(3), 427–446 (2009)
Magirius, M., Mundhenk, M., Palenta, R.: The complexity of primal logic with disjunction. IPL 115(5), 536–542 (2015)
McAllester, D.A.: Automatic Recognition of Tractability in Inference Relations. JACM 40(2), 284–303 (1993)
Ramanujam, R., Sundararajan, V., Suresh, S.P.: Extending Dolev-Yao with assertions. In: Prakash, A., Shyamasundar, R. (eds.) ICISS 2014. LNCS, vol. 8880, pp. 50–68. Springer, Heidelberg (2014)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions and composed keys is NP-complete. TCS 299, 451–475 (2003)
Sakharov, A.: Median logic. Technical report, St. Petersberg Mathematical Society (2004). http://www.mathsoc.spb.ru/preprint/2004/index.html
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Ramanujam, R., Sundararajan, V., Suresh, S.P. (2016). The Complexity of Disjunction in Intuitionistic Logic. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2016. Lecture Notes in Computer Science(), vol 9537. Springer, Cham. https://doi.org/10.1007/978-3-319-27683-0_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-27683-0_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27682-3
Online ISBN: 978-3-319-27683-0
eBook Packages: Computer ScienceComputer Science (R0)