Formally defining security properties with relations on streams

Citations of this article
Mendeley users who have this article in their library.


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).

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free