A formal approach for checking security properties in SecSpaces

SecSpaces is a Linda-like coordination model whose aim is to provide a support for secure coordination in Open System applications. Substantially it provides a methodology to restrict the access to the objects stored in the shared dataspace. In this paper we introduce a formal language for representing systems interacting via SecSpaces primitives and its operational semantics. Moreover in this context we consider a notion of observational equivalence, namely testing equivalence. In order to evaluate the adequacy of the model for limiting the access to the shared dataspace, we present some examples of interaction protocols that can be used to obtain some security properties (e.g., authentication or privacy of a datum).