Refinement-based design of a group-centric secure information sharing model

This paper presents a formal, state machine-based specification (stateful specification) of a group-centric secure information sharing (g-SIS) model. The stateful specification given here is a refinement of a prior specification that is given in first-order linear temporal logic (FOTL). Such FOTL specification defines authorization based solely on group operations, but gives little guidance regarding implementation. The current specification is the result of a second step in a multi-step design process that separates concerns and provides multiple opportunities to detect unintended policy characteristics. We show that our stateful specification is consistent with the prior FOTL specification by using a combination of model-checking and manual techniques.