Semantics for Interactive Sequential Systems and Non-Interference Properties

An interactive system is a system that allows communication with the users. This communi- cation is modeled through input and output actions. Input actions are controllable by a user of the system, while output actions are controllable by the system. Standard semantics for sequen- tial system [1, 2] are not suitable in this context because they do not distinguish between the different kinds of actions. Applying a similar approach to the one used in [2] we define seman- tics for interactive systems. In this setting, a particular semantic is associated with a notion of observability. These notions of observability are used as parameters of a general definition of non-interference. We show that some previous versions of the non-interference property based on traces semantic, weak bisimulation and refinement, are actually instances of the observability- based non-interference property presented here. Moreover, this allows us to show some results in a general way and to provide a better understanding of the security properties