Refinement-based Design of a Group-centric Secure Information Sharing Model

dc.contributor.authorZhao, Wanying
dc.contributor.authorNiu, Jianwei
dc.contributor.authorWinsborough, William H.
dc.date.accessioned2023-10-26T15:21:46Z
dc.date.available2023-10-26T15:21:46Z
dc.date.issued2011-12
dc.description.abstractThis paper presents a formal, state machine-based specification (stateful specification) of a high assurance, secure information-sharing policy. The policy is group-centric; users join and leave groups, objects are added and removed (group operations). Users gain access to objects via membership relationships they have or have had with groups that contain or have contained those objects. The stateful specification given here is a refinement of a prior specification that is given in first-order linear temporal logic (FOTL). The prior FOTL specification defines authorization based solely on event histories, 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 with respect to the action sequences it permits and the authorization decisions it renders. For verification purposes we use a combination of model-checking and manual techniques.
dc.description.departmentComputer Science
dc.identifier.urihttps://hdl.handle.net/20.500.12588/2179
dc.language.isoen_US
dc.publisherUTSA Department of Computer Science
dc.relation.ispartofseriesTechnical Report; CS-TR-2011-016
dc.subjectaccess control
dc.subjectformal specification
dc.subjectformal verification
dc.subjectsystem refinement
dc.subjectsecure information sharing
dc.titleRefinement-based Design of a Group-centric Secure Information Sharing Model
dc.typeTechnical Report

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Zhao_et_al_CS-TR-2011-016.pdf
Size:
290.71 KB
Format:
Adobe Portable Document Format

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.86 KB
Format:
Item-specific license agreed upon to submission
Description: