Reference from ESORICS proceedings

6th European Symposium on Research in Computer Security (ESORICS 2000)

Unwinding Possibilistic Security Properties

Heiko Mantel

Keywords : security models, information flow, unwinding, refinement

Abstract : Unwinding conditions are helpful to prove that deterministic systems fulfill non-interference. In order to generalize non-interference to non-deterministic systems various possibilistic security properties have been proposed. In this paper, we present generic unwinding conditions which are applicable to a large class of such security properties. That these conditions are sufficient to ensure security is demonstrated by unwinding theorems. In certain cases, they are also necessary. The practical usefulness of our results is illustrated by instantiating the generic unwinding conditions for well-known security properties. Furthermore, similarities of proving security with proving refinement are identified which results in proof techniques which are correct as well as complete.

(Pages 238-254)

Proceedings table of contents