A step towards formal reasoning on abstract security properties

Formal approaches have been used traditionally to verify whether systems fulfill certain property especially in the field of model checking. However, those formal specifications are strongly biased by the underlying verification model instead of representing the intuitive concepts. And few people researches on relations between different properties. In this paper, we introduce the formal specification of some properties of system and present a different reasoning approach to establish relations of abstract security properties based on abstract system operating model for the first time. We show the approach is feasible by examples of four security properties, which are reliability, stability, survivability and availability, related to system design and implementation. And we conclude that availability entails the other three properties, that is, definition of availability is stronger than definition of other three properties.