Prerequisite confidentiality

摘要

We have developed a modelling scheme that is based upon event systems in order to study prerequisite confidentiality. The structure of the event traces is captured by formal languages and grammars. This provides a convenient and mathematically well-founded means for dealing with component specifications. The externally visible-behaviour of a component, including causal relationships between events, and possible nondeterminism, is successfully modelled using the approach. It is then possible to restrict the grammatical specification in such a way that the desired confidentiality property is satisfied. Since all of the grammars used in the specification technique fall into a particular class, we show that it is always possible to construct a recognizer that can be used to identify valid event sequences or determine whether an event sequence satisfies a desired property.