Formal Models for Group-Centric Secure Information Sharing

We develop the foundations for a theory of Group-Centric Secure Information Sharing (g-SIS), characterize a specific family of models in this arena and identify several directions in which this theory can be extended. The traditional approach to information sharing, characterized as Dissemination-Centric in this paper, focuses on attaching attributes and policies to an object (sometimes called “sticky policies”) as it is disseminated from producers to consumers in a system. In contrast, Group-Centric sharing envisions bringing the subjects and objects together in a group to facilitate sharing. The metaphor is that of a secure meeting room where participants and information come together to enable parties to “share” information for some common purpose. We formalize the concept of an Information-Sharing Group using Linear Temporal Logic (LTL), by specifying g-SIS properties. We begin with a core set of properties (Simultaneity, Provenance, Persistence, Availability, etc.) that any g-SIS model must satisfy. Next we identify additional properties regarding specific variations of group operations (Strict, Liberal, Lossy, Lossless, etc.). Finally, we specify the correct authorization behavior for a sub-family of g-SIS specifications using LTL and formally prove that the specifications satisfy the properties using the model checker NuSMV.