Options
Unwinding possibilistic security properties
Publikationstyp
Conference Paper
Publikationsdatum
2000-10
Sprache
English
Author
Mantel, Heiko
First published in
Number in series
1895 LNCS
Start Page
238
End Page
254
Citation
Lecture Notes in Computer Science 1895 LNCS: 238-254 (2000)
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
Springer
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.
Schlagworte
Information flow
Refinement
Security models
Unwinding
DDC Class
004: Informatik