2002 · 152 citations · 16 references
ComputingComputer ScienceComputer SecurityFormal MethodsSet TheoryData SecurityInformation-theoretic SecurityEvent Sequence AnalysisEvent Sequence DiagramsEvent Sequence ReasoningFormal Verification Of Security PropertiesInformation Flow ControlInterleavingPartial OrderingTruth Predicate
We present a general theory of possibilistic security properties. We show that we can express a security property as a predicate that is true of every set containing all the traces with the same low level event sequence. Given this security predicate, we show how to construct a partial ordering of security properties. We also discuss information flow and present the weakest property such that no information can flow from high level users to low level users. Finally, we present a comparison of our framework and McLean's (1994) Selective Interleaving Functions framework.
16
Security Policies and Security Models
Joseph A. Goguen, José Meseguer · 1982 · 2.1K citations
Bowen Alpern, Fred B. Schneider · Information Processing Letters · 1985 · 1K citations
Unwinding and Inference Control
Joseph A. Goguen, José Meseguer · 1984 · 426 citations
Noninterference and the composability of security properties
Daryl McCullough · 2003 · 264 citations