Specification and Verification of Security Requirements in Decentralized CSCW Systems

In this paper, we present a specification model and a verification methodology for security policies in distributed CSCW systems. To express security and coordination requirements in decentralized CSCW systems, a role-based specification model is developed. We show how dynamic security requirements in collaboration environments are expressed in this specification model. Given global security requirements, verification of a specification ensures correctness and consistency of the specification. The goal of our methodology is to ensure that sensitive security requirements cannot be violated in decentralized management of a collaboration involving multiple security domains where all the participating users in the collaboration may not be trusted. We have utilized finite-state based model checking for static verification of security requirements. Several verification models are developed to check security properties, such as task-flow constraints, information flow or confidentiality, and assignment of administrative privileges