Abstract
We present a translation from a logic of access control with a “says” operator to the classical modal logic S4. We prove that the translation is sound and complete. We also show that it extends to logics with boolean combinations of principals and with a “speaks for” relation. While a straightforward definition of this relation requires second-order quantifiers, we use our translation for obtaining alternative, quantifier-free presentations. We also derive decidability and complexity results for the logics of access control.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M.: Logic in access control. In: Proceedings of the 18th Annual Symposium on Logic in Computer Science (LICS 2003), pp. 228–233 (June 2003)
Abadi, M.: Access control in a core calculus of dependency. Electronic Notes in Theoretical Computer Science, Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin 172, 5–31 (April 2007)
Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems 15(4), 706–734 (1993)
Abadi, M., Wobber, T.: A logical account of NGSCB. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 1–12. Springer, Heidelberg (2004)
Alechina, N., Mendler, M., de Paiva, V., Ritter, E.: Categorical and kripke semantics for constructive S4 modal logic. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 292–307. Springer, Heidelberg (2001)
Appel, A.W., Felten, E.W.: Proof-carrying authentication. In: Proceedings of the 6th ACM Conference on Computer and Communications Security, pp. 52–62 (November 1999)
Bauer, L., Garriss, S., McCune, J.M., Reiter, M.K., Rouse, J., Rutenbar, P.: Device-enabled authorization in the Grey system. In: Zhou, J., López, J., Deng, R.H., Bao, F. (eds.) ISC 2005. LNCS, vol. 3650, pp. 431–445. Springer, Heidelberg (2005)
Bauer, L.: Access Control for the Web via Proof-Carrying Authorization. PhD thesis, Princeton University (November 2003)
Bauer, L., Garriss, S., Reiter, M.K.: Distributed proving in access-control systems. In: Proceedings of the 2005 Symposium on Security and Privacy, pp. 81–95 (May 2005)
Becker, M.Y., Fournet, C., Gordon, A.D.: Design and semantics of a decentralized authorization language. In: 20th IEEE Computer Security Foundations Symposium, pp. 3–15 (2007)
Benton, P.N., Bierman, G.M., de Paiva, V.C.V.: Computational types from a logical perspective. Journal of Functional Programming 8(2), 177–193 (1998)
Cardelli, L.: Type systems. In: Tucker, A.B. (ed.) The Computer Science and Engineering Handbook, ch. 103, pp. 2208–2236. CRC Press, Boca Raton, FL (1997)
Cederquist, J.G., Corin, R., Dekker, M.A.C., Etalle, S., den Hartog, J.I., Lenzini, G.: Audit-based compliance control. Int. J. Inf. Secur. 6(2), 133–151 (2007)
Cirillo, A., Jagadeesan, R., Pitcher, C., Riely, J.: Do as I SaY! programmatic access control with explicit identities. In: 20th IEEE Computer Security Foundations Symposium, pp. 16–30 (July 2007)
Curry, H.B.: The elimination theorem when modality is present. Journal of Symbolic Logic 17(4), 249–265 (1952)
DeTreville, J.: Binder, a logic-based security language. In: Proceedings of the 2002 IEEE Symposium on Security and Privacy, pp. 105–113 (May 2002)
Fairtlough, M., Mendler, M.V.: Propositional lax logic. Information and Computation 137(1), 1–33 (1997)
Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization in distributed systems. In: 20th IEEE Computer Security Foundations Symposium, pp. 31–45 (2007)
Garg, D., Bauer, L., Bowers, K.D., Pfenning, F., Reiter, M.K.: A linear logic of authorization and knowledge. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 297–312. Springer, Heidelberg (2006)
Garg, D., Pfenning, F.: Non-interference in constructive authorization logic. In: Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW 19), pp. 283–296 (2006)
Girard, J.-Y.: Interprétation Fonctionnelle et Elimination des Coupures de l’Arithmétique d’Ordre Supérieur. Thèse de doctorat d’état, Université Paris VII (June 1972)
Gödel, K.: Eine Interpretation des intuitionistischen Aussagenkalkuls. Ergebnisse eines mathematischen Kolloquiums 8, 39–40 (1933)
Howe, J.M.: Proof search in lax logic. Mathematical Structures in Computer Science 11(4), 573–588 (2001)
Hughes, G.E., Cresswell, M.J.: An Introduction to Modal Logic. Methuen Inc., New York (1968)
Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing 6(3), 467–480 (1977)
Lampson, B., Abadi, M., Burrows, M., Wobber, E.: Authentication in distributed systems: Theory and practice. ACM Transactions on Computer Systems 10(4), 265–310 (1992)
Lampson, B.W.: Protection. In: Proceedings of the 5th Princeton Conference on Information Sciences and Systems, pp. 437–443 (1971)
Lampson, B.W.: Computer security in the real world. IEEE Computer 37(6), 37–46 (2004)
Lesniewski-Laas, C., Ford, B., Strauss, J., Kaashoek, M.F., Morris, R.: Alpaca: Extensible authorization for distributed services. In: 14th ACM Conference on Computer and Communications Security, pp. 432–444 (2007)
Li, N., Grosof, B.N., Feigenbaum, J.: Delegation logic: A logic-based approach to distributed authorization. ACM Transactions on Information and System Security 6(1), 128–171 (2003)
Li, N., Mitchell, J.C.: Datalog with constraints: A foundation for trust management languages. In: Proceedings of the Fifth International Symposium on Practical Aspects of Declarative Languages, pp. 58–73 (2003)
Li, N., Mitchell, J.C., Winsborough, W.H.: Beyond proof-of-compliance: security analysis in trust management. J. ACM 52(3), 474–514 (2005)
Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991)
Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11, 511–540 (2001)
Wobber, E., Abadi, M., Burrows, M., Lampson, B.: Authentication in the Taos operating system. ACM Transactions on Computer Systems 12(1), 3–32 (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Garg, D., Abadi, M. (2008). A Modal Deconstruction of Access Control Logics. In: Amadio, R. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2008. Lecture Notes in Computer Science, vol 4962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78499-9_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-78499-9_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78497-5
Online ISBN: 978-3-540-78499-9
eBook Packages: Computer ScienceComputer Science (R0)