Message-Id: <9102212224.AA05574@oxalis.eecs.ucdavis.edu>
To: cant@au.oz.dsto.itd (Tony Cant)
Cc: info-hol@edu.ucdavis.eecs.clover, foss@edu.ucdavis.eecs.oxalis
Subject: Re: Security
In-Reply-To: Your message of Thu, 21 Feb 91 09:36:02 -0600. <9102202306.AA14745@itd0.dsto.oz>
Date: Thu, 21 Feb 91 14:24:26 -0800
From: foss@edu.ucdavis.eecs.oxalis

I have taken the work of D. McCullough and his colleagues at Odyssey
Research and implemented a version of it in HOL.

Currently I have:
1) Implemented a theory of sequence.
2) Implemented a theory of event systems.
3) Implemented a theory of restrictiveness, generalized from McCullough
   - Shown that restrictiveness satisfies the Hook-up property 
     (if two components are restrictive thentheir hook-up is restrictive)
   - Developed a set of generic classes of components
   - Started showing under which conditions these classes are restrictive
   - Instantiated components for these classes and shown that they
     are restrictive
   - Proven a simple distributed system (ala Rusbhy & Randell) satisfies
     restrictiveness.


\bibitem{McCullough88b}
D. McCullough.
\newblock {\it Foundations of Ulysses: The Theory of Security}.
\newblock Technical Report~RADC-TR-87-222, Odyssey Research Associates, Inc.,
  July 1988.

\bibitem{McCullough88a}
D. McCullough.
\newblock Noninterference and the composability of security properties.
\newblock {\it IEEE Conference on Security and Privacy}, 177--186, 1988.

\bibitem{McCullough87}
D. McCullough.
\newblock Specifications for multi-level security and a hook-up property.
\newblock {\it IEEE Conference on Security and Privacy}, 161--166, 1987.

\bibitem{Rushby83}
J. Rushby and B. Randell.
\newblock A distributed secure system.
\newblock {\it IEEE Computer}, 16(7):55--67, 1983.

\bibitem{Alves-Foss91b}
J. Alves-Foss and K. Levitt.
\newblock Verification of Secure Distributed Systems in Higher Order
  Logic: A Modular Approach Using Generic Components
\newblock {\it IEEE Conference on Security and Privacy}, {\sc to appear}, 1991.

-Jim Alves-Foss