On a formal framework for security properties

A new approach to property-based characterisation of security requirements is presented. The main goal is to provide a framework for the specification of a wide variety of security requirements with formal semantics in terms of security properties of a discrete model of a system. In contrast to previous approaches it is not focused on a special type of security property. The classical concept of “properties” comprising safety and liveness properties is extended to include security properties. Formalisations of authenticity, different types of non-repudiation and confidentiality are presented within the framework. Several examples illustrate the flexibility of this approach.