Formally defining security properties with relations on streams

  • Lotz V
  • 3


    Mendeley users who have this article in their library.
  • 3


    Citations of this article.


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.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Volkmar Lotz

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free