Server-process restrictiveness in HOL

Stephen H. Brackin, Shiu Kai Chin

Research output: Chapter in Book/Entry/PoemConference contribution

Abstract

Restrictiveness is a security property of multilevel systems, guaranteeing that a system’s behavior visible at one security level does not reveal the existence of inputs or outputs at other levels not dominated by this level. This paper gives a convenient language for specifying processes, an operational semantics for this language, and a collection of easy to understand, inductively defined security properties that can be used to substantially automate proving restrictiveness for buffered server processes specified in this language.

Original languageEnglish (US)
Title of host publicationHigher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings
EditorsJeffrey J. Joyce, Carl-Johan H. Seger
PublisherSpringer Verlag
Pages450-463
Number of pages14
ISBN (Print)9783540578260
DOIs
StatePublished - 1994
Event6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993 - Vancouver, Canada
Duration: Aug 11 1993Aug 13 1993

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume780 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993
Country/TerritoryCanada
CityVancouver
Period8/11/938/13/93

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Server-process restrictiveness in HOL'. Together they form a unique fingerprint.

Cite this