Specification and verification of security requirements in a programming model for decentralized CSCW systems

We present, in this paper, a role-based model for programming distributed CSCW systems. This model supports specification of dynamic security and coordination requirements in such systems. We also present here a model-checking methodology for verifying the security properties of a design expressed in this model. The verification methodology presented here is used to ensure correctness and consistency of a design specification. It is also used to ensure that sensitive security requirements cannot be violated when policy enforcement functions are distributed among the participants. Several aspect-specific verification models are developed to check security properties, such as task-flow constraints, information flow, confidentiality, and assignment of administrative privileges.