Skip to main content
SpringerLink
Log in
Book cover

HOL Users' Group Workshop

HUG 1994: Higher Order Logic Theorem Proving and Its Applications pp 65–80Cite as

Providing tractable security analyses in HOL

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 859))

Abstract

This paper describes tools that let HOL users, even unsophisticated ones, employ sophisticated HOL concepts in conveniently specifying system designs and proving that these designs have particular nondisclosure security properties. These tools include the Romulus Interface Process Specification Language (IPSL) and a translator for translating IPSL specifications into HOL90.

Supported by Rome Laboratory Contract F30602-90-C-0092

The author wishes to thank Shiu-Kai Chin, David Rosenthal, Randy Calistri-Yeh, Doug Long, and the referees for helpful comments.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. Alves-Foss and K. Levitt. A Model of Event Systems in Higher Order Logic: Sequence and Event System Theories. Technical Report CSE-90-45, Division of Computer Science, University of California, Davis, November 1990.

    Google Scholar 

  2. J. Alves-Foss and K. Levitt. A Security Property in Higher Order Logic: Restrictiveness and Hook-Up Theories. Technical Report CSE-90-46, Division of Computer Science, University of California, Davis, December 1990.

    Google Scholar 

  3. J. Alves-Foss and K. Levitt. Mechanical Verification of Secure Distributed Systems in Higher Order Logic. In Proceedings of the 1991 International Meeting on Higher Order Logic Theorem Proving and its Applications, pages 263–278, 1991.

    Google Scholar 

  4. J. Alves-Foss and K. Levitt. Verification of Secure Distributed Systems in Higher Order Logic: A Modular Approach Using Generic Components. In Proceedings of the Symposium on Security and Privacy, pages 122–135, Oakland, CA, 1991. IEEE.

    Google Scholar 

  5. S. Brackin and S-K Chin. Server-process restrictiveness in HOL. In HOL User's Group Workshop, Vancouver, Canada, August 1993. Springer Verlag.

    Google Scholar 

  6. Department of Defense. Trusted Computer System Evaluation Criteria, December 1985. DoD-5200.28-STD.

    Google Scholar 

  7. Joseph A. Goguen and José Meseguer. Security policy and security models. In Proceedings of the Symposium on Security and Privacy, pages 11–20, Oakland, CA, April 1982. IEEE.

    Google Scholar 

  8. C. A. R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, Englewood Cliffs, NJ, 1985.

    Google Scholar 

  9. D. McCullough. Specifications for multilevel security and a hook-up property. In Proceedings of the Symposium on Security and Privacy, pages 161–166, Oakland, CA, April 1987. IEEE.

    Google Scholar 

  10. D. McCullough. Foundations of Ulysses: The theory of security. Technical Report RADC-TR-87-222, Rome Air Development Center, May 1988.

    Google Scholar 

  11. D. McCullough. Noninterference and the composability of security properties. In Proceedings of the Symposium on Security and Privacy, pages 177–186, Oakland, CA, April 1988. IEEE.

    Google Scholar 

  12. R. Milner. Communication and Concurrency. Prentice-Hall, NY, 1990.

    Google Scholar 

  13. ORA. Romulus Theories. Technical Report TM-94-0016, Odyssey Research Associates, Ithaca, NY, March 1994.

    Google Scholar 

  14. ORA. Romulus Library of Models. Technical Report TM-94-0017, Odyssey Research Associates, Ithaca, NY, March 1994.

    Google Scholar 

  15. ORA. Romulus User's Manual. Technical Report TM-94-0018, Odyssey Research Associates, Ithaca, NY, March 1994.

    Google Scholar 

  16. ORA. Romulus Overview. Technical Report TM-94-0019, Odyssey Research Associates, Ithaca, NY, March 1994.

    Google Scholar 

  17. D. Rosenthal. An approach to increasing the automation of the verification of security. In Proceedings of Computer Security Foundations Workshop, pages 90–97, Franconia, NH, June 1988. The MITRE Corporation, M88-37.

    Google Scholar 

  18. D. Rosenthal. Implementing a verification methodology for McCullough security. In Proceedings of Computer Security Foundations Workshop II, pages 133–140, Franconia, NH, June 1989. IEEE Computer Society Press.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Odyssey Research Associates, 301 Dates Drive, 14850, Ithaca, NY

    Stephen H. Brackin

Authors
  1. Stephen H. Brackin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Thomas F. Melham Juanito Camilleri

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brackin, S.H. (1994). Providing tractable security analyses in HOL. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_35

Download citation

  • DOI: https://doi.org/10.1007/3-540-58450-1_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58450-6

  • Online ISBN: 978-3-540-48803-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation