Providing tractable security analyses in HOL
Stephen H. Brackin1
| (1) |
Odyssey Research Associates, 301 Dates Drive, 14850 Ithaca, NY |
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.
References secured to subscribers.