Library FSSecModel.InitialState
Require Export SFSstate.
Set Implicit Arguments.
Unset Strict Implicit.
Section InitialState.
Parameter SysGroups : GRPNAME → set SUBJECT.
Parameter SysPrimaryGrp : SUBJECT → GRPNAME.
Parameter SysSubjectSC : set (SUBJECT × SecClass).
Parameter SysAllGrp SysRootGrp SysSecAdmGrp : GRPNAME.
Axiom SysSubjectSCIsPARTFUNC : IsPARTFUNC SUBeq_dec SysSubjectSC.
Axiom RootBelongsToRootGrp : set_In root (SysGroups SysRootGrp).
Axiom RootBelongsToAllGrp : set_In root (SysGroups SysAllGrp).
Axiom SecofrBelongsToSecAdmGrp : set_In root (SysGroups SysSecAdmGrp).
Axiom SecofrBelongsToAllGrp : set_In root (SysGroups SysAllGrp).
Definition InitState : SFSstate :=
mkSFS SysGroups SysPrimaryGrp SysSubjectSC SysAllGrp SysRootGrp
SysSecAdmGrp (empty_set (OBJECT × SecClass))
(empty_set (OBJECT × AccessCtrlListData))
(empty_set (OBJECT × ReadersWriters)) (empty_set (OBJECT × FILECONT))
(empty_set (OBJECT × DIRCONT)).
End InitialState.
Hint Resolve SysSubjectSCIsPARTFUNC.
Set Implicit Arguments.
Unset Strict Implicit.
Section InitialState.
Parameter SysGroups : GRPNAME → set SUBJECT.
Parameter SysPrimaryGrp : SUBJECT → GRPNAME.
Parameter SysSubjectSC : set (SUBJECT × SecClass).
Parameter SysAllGrp SysRootGrp SysSecAdmGrp : GRPNAME.
Axiom SysSubjectSCIsPARTFUNC : IsPARTFUNC SUBeq_dec SysSubjectSC.
Axiom RootBelongsToRootGrp : set_In root (SysGroups SysRootGrp).
Axiom RootBelongsToAllGrp : set_In root (SysGroups SysAllGrp).
Axiom SecofrBelongsToSecAdmGrp : set_In root (SysGroups SysSecAdmGrp).
Axiom SecofrBelongsToAllGrp : set_In root (SysGroups SysAllGrp).
Definition InitState : SFSstate :=
mkSFS SysGroups SysPrimaryGrp SysSubjectSC SysAllGrp SysRootGrp
SysSecAdmGrp (empty_set (OBJECT × SecClass))
(empty_set (OBJECT × AccessCtrlListData))
(empty_set (OBJECT × ReadersWriters)) (empty_set (OBJECT × FILECONT))
(empty_set (OBJECT × DIRCONT)).
End InitialState.
Hint Resolve SysSubjectSCIsPARTFUNC.
