In this paper we show how to formally define security properties in the framework of FOCUS, a general approach for the specification and verification of reactive systems. In FOCUS, systems are composed of components that communicate asynchronously via unidirectional channels, with their semantics being defined by relating complete input and output histories modeled by streams. By taking into account practically established method from security engineering, we define security as being a relation between the system and a modification of the system describing relevant attack situations. The modification is called a threat scenario. The relation specifies the kind of deviation in system behaviour that is tolerable with respect to the given protection needs. We introduce generic relations covering authenticity, integrity, availability and confidentiality. By comparing our characterization with security notions occurring in the literature and by sketching properties of our definitions we argue that our formalization of security is reasonable and adequate. © 2000 Published by Elsevier Science B.V.
Lotz, V. (2000). Formally defining security properties with relations on streams. In Electronic Notes in Theoretical Computer Science (Vol. 32, pp. 26–41). https://doi.org/10.1016/S1571-0661(04)00093-3