A logic for reasoning about security

ABSTRACT

A formal framework called Security Logic (SL) is developed for specifying and reasoning about security policies and for verifying that system designs adhere to such policies. Included in this modal logic framework are definitions of knowledge, permission, and obligation. Permission is used to specify secrecy policies and obligation to specify integrity policies. The combination of policies is addressed and examples based on policies from the current literature are given.

REFERENCES

• 1: E A Ashcroft , R Jagannathan, Operator nets, Proc. of the IFIP TC 10 working conference on Fifth generation computer architectures, p.177-201, October 1986, Manchester, United Kingdom
• 2: Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
• 3: Michael Burrows , Martin Abadi , Roger Needham, A logic of authentication, ACM Transactions on Computer Systems (TOCS), v.8 n.1, p.18-36, Feb. 1990 [doi>10.1145/77648.77649]
• 4: BIB& K. J. Integrity considerations for secure computer systems. Tech. Rep. TR-3153, MITRE Corp., April 1977.
• 5: BELL, D. E., AND LAPADULA, L.J. Secure computer systems: Mathematical foundations and model. Tech. Rep., MITRE Corp., Bedford, Mass., 1974.
• 6: Michael Burrows , Martín Abadi , Roger M. Needham, Authentication: A Practical Study in Belief and Action, Proceedings of the 2nd Conference on Theoretical Aspects of Reasoning about Knowledge, p.325-342, March 01, 1988
• 7: COMMUNICATIONS SECURITY ESTABLISHMENT, DND. Canadian Trusted Computer Product Evaluation Criteria Workshop (Ottawa, Ont., Aug. 1988).
• 8: CLARK, D. n., AND WILSON, D. R. A comparison of commercial and military computer security policies. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1987). IEEE, New York, 1987, 184-194.
• 9: Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
• 10: EMERSON, E. A., AND HALPERN, J.Y. "Sometimes" and "not never" revisited. In 9th Annual ACM Symposium on Prznciples of Programming Languages. ACM, New York, 1982, 127-139.
• 11: Morrie Gasser, Building a secure computer system, Van Nostrand Reinhold Co., New York, NY, 1988
• 12: GOGUEN, J. A., AND MESEGUER, J. SecuriW policies and security models. In IEEE Symposium on Securzty and Privacy (Oakland, Calif., April 1982). IEEE, New York, 1982, 11-20.
• 13: Janice I. Glasgow , Glenn H. MacEwen, The development and proof of a formal specification for a multilevel secure system, ACM Transactions on Computer Systems (TOCS), v.5 n.2, p.151-184, May 1987 [doi>10.1145/13677.22724]
• 14: GLASGOW, J. I., AND MACEWEN, G. H. Reasoning about knowledge in multilevel secure distributed systems. In Proceedings of the IEEE Symposium on Securtty and Privacy (Oakland, Calif., 1988). IEEE, New York, 1988, 122-128.
• 15: GLASGOW, J. I., AND MACEWEN, G.H. Obligation as the basis of integrity specification. In Proceedings of the IEEE Symposium on Securzty and Privacy (Oakland, Calif.,), IEEE, New York, 1982-91.
• 16: GLASGOW, J. I., AND MACEWEN, G.H. Obligation as the basis of integrity specification. In Proceedings of the Computer Security Foundattons Workshop (Franconia, N.H.). MITRE Corp., 1988-91.
• 17: GLASGOW, J. I., AND MACEWEN, G.H. Obligation as the basis of integrity specification. In Proceedings of the Computer Security Foundattons Workshop (Franconia, N. H., June 1989). MITRE Corp., 1989, 64-70.
• 18: GLASGOW, J. I., AND MACEWEN, G.H. An operator net model for distributed systems. J. Distrtbuted Syst. 3, 4 (Sept. 1989), 196-209.
• 19: GLASGOW, J. I., ANn MACEWEN, G.H. A logic for reasoning about security. In Proceedings of the Computer Security Foundations Workshop (Franconia, N.H., June 1990). IEEE, New York, 1990.
• 20: GLASGOW, J. I., MACEWEN, G. H., AND PANANGADEN, P. Reasoning about knowledge and permission in secure distributed systems. In Proceedtngs of the Computer Security Foundations Workshop (Franconia, N.H., 1988). IEEE, New York, 1988, 139 146. Also appears in IEEE Cipher.
• 21: GLASGOW, J. I., MACEWEN, G. H., AND PANANGADEN, P. Security by permission in databases. In Database Security H: Status and Prospects. Elsevier North-Holland, Amsterdam, 1988, 197-205.
• 22: GUTTMAN, J. D., AND NADEL, M. E. What needs security? In Proceedings of the Computer Security Foundations Workshop (Franconia, N.H., June 1988), 34-57.
• 23: HALPERN, J. Reasoning about knowledge. In Annual Reviews of Computer Science, Annual Reviews Inc., 1987, 21-35.
• 24: HINTAKKA, J. Knowledge and Belief. Cornell University Press, 1962.
• 25: Joseph Y. Halpern , Yoram Moses, Knowledge and common knowledge in a distributed environment, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.50-61, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806735]
• 26: Dale M. Johnson , F. Javier Thayer, Stating security requirements with tolerable sets, ACM Transactions on Computer Systems (TOCS), v.6 n.3, p.284-295, Aug. 1988 [doi>10.1145/45059.214409]
• 27: JOHNSON, D. M., AND THAYER, F.J. Security and the composition of machines. In Proceedings of the Computer Security Foundations Workshop (Franconia, N.H., June 1988), 72 89.
• 28: KmPKE, S. Semantical considerations of modal logic. Acta Philosophica Fennica 16 (1963), 83 94.
• 29: Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567463]
• 30: Carl E. Landwehr, Formal Models for Computer Security, ACM Computing Surveys (CSUR), v.13 n.3, p.247-278, Sept. 1981 [doi>10.1145/356850.356852]
• 31: LUNT, T. F. ET AL. The Seaview formal security policy model. Tech. Rep., SRI International, Computer Science Lab., Menlo Park, Calif, Feb. 1989.
• 32: T. F. Lunt , D. E. Denning , R. R. Schell , M. Heckman , W. R. Shockley, The SeaView Security Model, IEEE Transactions on Software Engineering, v.16 n.6, p.593-607, June 1990 [doi>10.1109/32.55088]
• 33: MECULLOUGH, A. D. Specifications for multi-level security and a hook-up property. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1987), IEEE, New York, 1987, 161-166.
• 34: MCCULLOUGH, A. D. Covert channels and degrees of insecurity. In Proceedings of the Computer Security Foundations Workshop (Franconia, N.H., June 1988), i 33.
• 35: MCCULLOUGH, A. D. Non-interference and the composability of security properties. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1988), IEEE, New York, 1988, 177-186.
• 36: MCLEAN, J. Reasoning about security models. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1987), IEEE, New York, 1987, 123-131.
• 37: MCLEAN, J. The algebra of security. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1988), IEEE, New York, 1988, 2-7.
• 38: MOSER, L. A logic of knowledge and belief for reasoning about computer security. In Proceedings of the Computer Security Foundattons Workshop H (Franconia, N.H., 1989), 57-63.
• 39: MAcEWEN, G. H., POON, V. W. W., AND GLASGOW, J.I. A model for multilevel security based on operator nets. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1987), IEEE, New York, 1987, 150-160.
• 40: NATIONAL COMPUTER SECURITY CENTER. Workshop on Integrity Policy in Computer Information Systems (Waltham, Mass., Oct. 1987).
• 41: Proceedings of the Natzonal Computer Security Conference, Dept. of Defense, 1984-88.
• 42: PNUELI, A. The temporal logic of concurrent programs. Theor. Comput. Sc~. 13 (1981), 45 60.
• 43: PRIOR, A. Tzme and Modality. Oxford University Press, 1957.
• 44: RANGAN, P.V. An axiomatic basis of trust in distributed systems. In Proceedings of the 1988 IEEE Computer Society Symposium on Security and Prwacy (Oakland, Calif., 1988), 204-211.
• 45: J. M. Rushby, Design and verification of secure systems, ACM SIGOPS Operating Systems Review, v.15 n.5, p.12-21, December 1981
• 46: SUTHERLAND, A. D. A model of information. In Procee&ngs of 9th Natwnal Computer Security Conference (Gaithersburg, Md., Sept. 1986), Dept. of Defense, 175-183.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS

  H. Information Systems
  H.2 DATABASE MANAGEMENT

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS

General Terms:
Security, Theory

Keywords:
composition knowledge, integrity, logic, obligation, permission, policy, possible-worlds, secrecy, security, time