| Global Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(475 entries) |
| Tactic Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(7 entries) |
| Axiom Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(42 entries) |
| Lemma Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(153 entries) |
| Constructor Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(99 entries) |
| Inductive Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(32 entries) |
| Definition Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(91 entries) |
| Module Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(51 entries) |
Global Index
A
ACL [constructor, in ModelProperties]
AclChanged [inductive, in ModelProperties]
ACLeq_dec [axiom, in SFSstate]
ACLGrp [constructor, in DACandMAC]
ACLOwner [constructor, in DACandMAC]
aclstat [inductive, in aclstat]
Aclstat [constructor, in SFSstate]
aclstat [module]
aclstatIsSecure [module]
AclstatOK [constructor, in aclstat]
AclstatPCP [lemma, in aclstatIsSecure]
AclstatPSP [lemma, in aclstatIsSecure]
AclstatPSS [lemma, in aclstatIsSecure]
AddEq [lemma, in FPF]
AddEq1 [lemma, in FPF]
AddRemEq [lemma, in FPF]
AddUsrGrpToAcl [constructor, in SFSstate]
addUsrGrpToAcl [inductive, in addUsrGrpToAcl]
addUsrGrpToAcl [module]
addUsrGrpToAclIsSecure [module]
addUsrGrpToAclOK [constructor, in addUsrGrpToAcl]
AddUsrGrpToAclPCP [lemma, in addUsrGrpToAclIsSecure]
AddUsrGrpToAclPSP [lemma, in addUsrGrpToAclIsSecure]
AddUsrGrpToAclPSS [lemma, in addUsrGrpToAclIsSecure]
addUsrGrpToAcl_acl [definition, in addUsrGrpToAcl]
AllWaysIncluded [lemma, in ListFunctions]
AuxiliaryLemmas [module]
Aux1 [lemma, in AuxiliaryLemmas]
B
BasicSecurityTheorem [lemma, in ModelLemmas]
BreakSS [tactic definition, in AuxiliaryLemmas]
BYTEeq_dec [axiom, in SFSstate]
C
Categ [constructor, in ModelProperties]
CATEGORY [axiom, in SFSstate]
ChangeGroupO [definition, in setACLdata]
ChangeGroupR [definition, in setACLdata]
ChangeGroupW [definition, in setACLdata]
ChangeUserR [definition, in setACLdata]
ChangeUserW [definition, in setACLdata]
Chmod [constructor, in SFSstate]
chmod [inductive, in chmod]
chmod [module]
chmodIsSecure [module]
ChmodOK [constructor, in chmod]
ChmodPCP [lemma, in chmodIsSecure]
ChmodPSP [lemma, in chmodIsSecure]
ChmodPSS [lemma, in chmodIsSecure]
chmod_acl [definition, in chmod]
chobjsc [inductive, in chobjsc]
Chobjsc [constructor, in SFSstate]
chobjsc [module]
chobjscIsSecure [module]
ChobjscPCP [lemma, in chobjscIsSecure]
ChobjscPSP [lemma, in chobjscIsSecure]
ChobjscPSS [lemma, in chobjscIsSecure]
Chobjsc_Corr [lemma, in AuxiliaryLemmas]
chobjsc_SC [definition, in chobjsc]
Chown [constructor, in SFSstate]
chown [inductive, in chown]
chown [module]
chownIsSecure [module]
ChownOK [constructor, in chown]
ChownPCP [lemma, in chownIsSecure]
ChownPSP [lemma, in chownIsSecure]
ChownPSS [lemma, in chownIsSecure]
chown_acl [definition, in chown]
chsobjscOK [constructor, in chobjsc]
Chsubsc [constructor, in SFSstate]
chsubsc [inductive, in chsubsc]
chsubsc [module]
chsubscIsSecure [module]
chsubscOK [constructor, in chsubsc]
ChsubscPCP [lemma, in chsubscIsSecure]
ChsubscPSP [lemma, in chsubscIsSecure]
ChsubscPSS [lemma, in chsubscIsSecure]
ChsubscPSS1 [lemma, in AuxiliaryLemmas]
Chsubsc_Corr [lemma, in AuxiliaryLemmas]
chsubsc_SC [definition, in chsubsc]
close [inductive, in close]
Close [constructor, in SFSstate]
close [module]
closeIsSecure [module]
CloseOK [constructor, in close]
ClosePCP [lemma, in closeIsSecure]
ClosePSP [lemma, in closeIsSecure]
ClosePSS [lemma, in closeIsSecure]
close_sm [definition, in close]
Close_smCorr [lemma, in AuxiliaryLemmas]
Close_smCorr2 [lemma, in AuxiliaryLemmas]
Close_smCorr3 [lemma, in AuxiliaryLemmas]
comp_mode [axiom, in stat]
ControlProperty [definition, in ModelProperties]
create [inductive, in create]
Create [constructor, in SFSstate]
create [module]
createIsSecure [module]
CreateOK [constructor, in create]
CreatePCP [lemma, in createIsSecure]
CreatePSP [lemma, in createIsSecure]
CreatePSS [lemma, in createIsSecure]
create_acl [definition, in create]
create_directories [axiom, in SFSstate]
create_files [axiom, in SFSstate]
create_oSC [definition, in create]
D
DACandMAC [module]
DACCtrlAttrHaveChanged [inductive, in ModelProperties]
DACSecureState [definition, in ModelProperties]
defaultState [axiom, in ModelLemmas]
delUsrGrpFromAcl [inductive, in delUsrGrpFromAcl]
DelUsrGrpFromAcl [constructor, in SFSstate]
delUsrGrpFromAcl [module]
delUsrGrpFromAclIsSecure [module]
delUsrGrpFromAclOK [constructor, in delUsrGrpFromAcl]
DelUsrGrpFromAclPCP [lemma, in delUsrGrpFromAclIsSecure]
DelUsrGrpFromAclPSP [lemma, in delUsrGrpFromAclIsSecure]
DelUsrGrpFromAclPSS [lemma, in delUsrGrpFromAclIsSecure]
delUsrGrpFromAcl_acl [definition, in delUsrGrpFromAcl]
DIRCONT [definition, in SFSstate]
DIRCONTeq_dec [lemma, in SFSstate]
Directory [constructor, in SFSstate]
DoAclstat [constructor, in TransFunc]
DoAddUsrGrpToAcl [constructor, in TransFunc]
DoChmod [constructor, in TransFunc]
DoChobjsc [constructor, in TransFunc]
DoChown [constructor, in TransFunc]
DoChsubsc [constructor, in TransFunc]
DoClose [constructor, in TransFunc]
DoCreate [constructor, in TransFunc]
DoDelUsrGrpFromAcl [constructor, in TransFunc]
DOM [definition, in FPF]
domacl [definition, in SFSstate]
domd [definition, in SFSstate]
domf [definition, in SFSstate]
DOMFuncRel [lemma, in FPF]
DOMFuncRel2 [lemma, in FPF]
DOMFuncRel3 [lemma, in FPF]
DOMFuncRel4 [lemma, in FPF]
DoMkdir [constructor, in TransFunc]
domOSC [definition, in SFSstate]
domsecmat [definition, in SFSstate]
domSSC [definition, in SFSstate]
DoOpen [constructor, in TransFunc]
DoOscstat [constructor, in TransFunc]
DoOwner_Close [constructor, in TransFunc]
DoRead [constructor, in TransFunc]
DoReaddir [constructor, in TransFunc]
DoRmdir [constructor, in TransFunc]
DoSscstat [constructor, in TransFunc]
DoStat [constructor, in TransFunc]
DoUnlink [constructor, in TransFunc]
DoWrite [constructor, in TransFunc]
E
empty_set [definition, in ListSet]
Eqfacl1 [lemma, in AuxiliaryLemmas]
Eqfacl2 [lemma, in AuxiliaryLemmas]
Eqfacl3 [lemma, in AuxiliaryLemmas]
Eqfacl4 [lemma, in AuxiliaryLemmas]
Eqfacl5 [lemma, in AuxiliaryLemmas]
EqfOSC1 [lemma, in AuxiliaryLemmas]
EqfOSC2 [lemma, in AuxiliaryLemmas]
EqfOSC3 [lemma, in AuxiliaryLemmas]
EqfOSC4 [lemma, in AuxiliaryLemmas]
EqfOSC5 [lemma, in AuxiliaryLemmas]
EqfOSC6 [lemma, in AuxiliaryLemmas]
EqfOSC7 [lemma, in AuxiliaryLemmas]
Eqfsecmat1 [lemma, in AuxiliaryLemmas]
Eqfsecmat2 [lemma, in AuxiliaryLemmas]
Eqfsecmat3 [lemma, in AuxiliaryLemmas]
EqfSSC1 [lemma, in AuxiliaryLemmas]
eq_sc [definition, in SFSstate]
eq_scIMPLYle_sc [lemma, in AuxiliaryLemmas]
eq_scSym [lemma, in AuxiliaryLemmas]
ExecuterIsOwner [inductive, in DACandMAC]
F
facl [definition, in SFSstate]
fdirs [definition, in SFSstate]
ffiles [definition, in SFSstate]
File [constructor, in SFSstate]
FILECONT [definition, in SFSstate]
FILECONTeq_dec [lemma, in SFSstate]
fOSC [definition, in SFSstate]
FPF [module]
front [definition, in ListFunctions]
fsecmat [definition, in SFSstate]
fSSC [definition, in SFSstate]
FuncPre1 [definition, in ModelProperties]
FuncPre2 [definition, in ModelProperties]
FuncPre3 [definition, in ModelProperties]
FuncPre4 [definition, in ModelProperties]
FuncPre5 [definition, in ModelProperties]
FuncPre6 [definition, in ModelProperties]
FuncPre7 [definition, in ModelProperties]
G
GeneralSecureState [definition, in ModelLemmas]
GO [constructor, in ModelProperties]
GR [constructor, in ModelProperties]
Group [constructor, in ModelProperties]
GRPeq_dec [axiom, in SFSstate]
GW [constructor, in ModelProperties]
I
Included [definition, in ListFunctions]
InDOMIsNotUndef [lemma, in FPF]
InDOMWhenAdd [lemma, in FPF]
InFileSystem [definition, in DACandMAC]
InitialState [module]
InitialStateIsSecure [lemma, in ModelLemmas]
InitState [definition, in InitialState]
IsEmpty [definition, in ListFunctions]
IsPARTFUNC [definition, in FPF]
IsUNIXOwner [inductive, in DACandMAC]
IUO [constructor, in DACandMAC]
L
last [definition, in ListFunctions]
Level [constructor, in ModelProperties]
le_sc [definition, in SFSstate]
Listeq_dec [lemma, in ListFunctions]
ListFunctions [module]
ListSet [module]
M
MACObjCtrlAttrHaveChanged [inductive, in ModelProperties]
MACSubCtrlAttrHaveChanged [inductive, in ModelProperties]
mkdir [inductive, in mkdir]
Mkdir [constructor, in SFSstate]
mkdir [module]
mkdirIsSecure [module]
MkdirOK [constructor, in mkdir]
MkdirPCP [lemma, in mkdirIsSecure]
MkdirPSP [lemma, in mkdirIsSecure]
MkdirPSS [lemma, in mkdirIsSecure]
mkdir_acl [definition, in mkdir]
mkdir_directories [axiom, in SFSstate]
mkdir_oSC [definition, in mkdir]
MODE [inductive, in SFSstate]
ModelLemmas [module]
ModelProperties [module]
MyDir [axiom, in SFSstate]
N
NEWDIR [definition, in mkdir]
NEWFILE [definition, in create]
NEWRW [definition, in close]
NEWRWOC [definition, in owner_close]
NoDACChange [lemma, in AuxiliaryLemmas]
NoDACChange2 [lemma, in AuxiliaryLemmas]
NoMACObjChange [lemma, in AuxiliaryLemmas]
NoMACObjChange2 [lemma, in AuxiliaryLemmas]
NoMACSubChange [lemma, in AuxiliaryLemmas]
NoMACSubChange2 [lemma, in AuxiliaryLemmas]
None [constructor, in mkdir]
None [constructor, in stat]
None [constructor, in owner_close]
None [constructor, in create]
None [constructor, in close]
None [constructor, in readdir]
None [constructor, in read]
None [constructor, in readdir]
None [constructor, in rmdir]
None [constructor, in read]
None [constructor, in sscstat]
None [constructor, in write]
None [constructor, in unlink]
NotInDOMIsUndef [lemma, in FPF]
NotInDOMIsUndef2 [lemma, in AuxiliaryLemmas]
NotInDOMIsUndef3 [lemma, in AuxiliaryLemmas]
O
OBJDeq_dec [axiom, in SFSstate]
OBJECT [definition, in SFSstate]
OBJeq_dec [lemma, in SFSstate]
OBJFeq_dec [axiom, in SFSstate]
ObjName [definition, in SFSstate]
OBJNAMEeq_dec [axiom, in SFSstate]
OBJTYPE [inductive, in SFSstate]
ObjType [definition, in SFSstate]
OBJTYPEeq_dec [lemma, in SFSstate]
OpDontChangeStPSP [tactic definition, in AuxiliaryLemmas]
OpDontChangeStPSS [tactic definition, in AuxiliaryLemmas]
open [inductive, in open]
Open [constructor, in SFSstate]
open [module]
openIsSecure [module]
OpenPCP [lemma, in openIsSecure]
OpenPSP [lemma, in openIsSecure]
OpenPSS [lemma, in openIsSecure]
OpenRead [constructor, in open]
OpenWrite [constructor, in open]
open_sm [definition, in open]
Open_smCorr21 [lemma, in AuxiliaryLemmas]
Open_smCorr22 [lemma, in AuxiliaryLemmas]
Open_smCorr3 [lemma, in AuxiliaryLemmas]
Open_smCorr31 [lemma, in AuxiliaryLemmas]
Open_smCorr32 [lemma, in AuxiliaryLemmas]
Operation [inductive, in SFSstate]
OSCeq_dec [axiom, in SFSstate]
Oscstat [constructor, in SFSstate]
oscstat [inductive, in oscstat]
oscstat [module]
oscstatIsSecure [module]
OscstatOK [constructor, in oscstat]
OscstatPCP [lemma, in oscstatIsSecure]
OscstatPSP [lemma, in oscstatIsSecure]
OscstatPSS [lemma, in oscstatIsSecure]
Owner [constructor, in ModelProperties]
ownerclose_sm [definition, in owner_close]
OwnerClose_smCorr2 [lemma, in AuxiliaryLemmas]
OwnerClose_smCorr3 [lemma, in AuxiliaryLemmas]
owner_close [inductive, in owner_close]
Owner_Close [constructor, in SFSstate]
owner_close [module]
owner_closeIsSecure [module]
Owner_CloseOK [constructor, in owner_close]
Owner_ClosePCP [lemma, in owner_closeIsSecure]
Owner_ClosePSP [lemma, in owner_closeIsSecure]
Owner_ClosePSS [lemma, in owner_closeIsSecure]
P
PARTFUNC [definition, in FPF]
PreDACRead [definition, in DACandMAC]
PreDACWrite [definition, in DACandMAC]
PreMAC [definition, in DACandMAC]
PreservesControlProp [definition, in ModelProperties]
PreStarPropRead [definition, in DACandMAC]
PreStarPropWrite [definition, in DACandMAC]
Prodeq_dec [lemma, in ListFunctions]
ProvePCP [tactic definition, in AuxiliaryLemmas]
R
RAN [definition, in FPF]
ransecmat [definition, in SFSstate]
read [inductive, in read]
Read [constructor, in SFSstate]
READ [constructor, in SFSstate]
read [module]
Readdir [constructor, in SFSstate]
readdir [inductive, in readdir]
readdir [module]
readdirIsSecure [module]
ReaddirOK [constructor, in readdir]
ReaddirPCP [lemma, in readdirIsSecure]
ReaddirPSP [lemma, in readdirIsSecure]
ReaddirPSS [lemma, in readdirIsSecure]
readIsSecure [module]
ReadOK [constructor, in read]
ReadPCP [lemma, in readIsSecure]
ReadPSP [lemma, in readIsSecure]
ReadPSS [lemma, in readIsSecure]
ReadWriteImpRead [lemma, in AuxiliaryLemmas]
ReadWriteImpWrite [lemma, in AuxiliaryLemmas]
RemEq [lemma, in FPF]
rmdir [inductive, in rmdir]
Rmdir [constructor, in SFSstate]
rmdir [module]
rmdirIsSecure [module]
RmdirOK [constructor, in rmdir]
RmdirPCP [lemma, in rmdirIsSecure]
RmdirPSP [lemma, in rmdirIsSecure]
RmdirPSS [lemma, in rmdirIsSecure]
rmdir_acl [definition, in rmdir]
rmdir_directories [axiom, in SFSstate]
rmdir_oSC [definition, in rmdir]
root [axiom, in SFSstate]
RootBelongsToAllGrp [axiom, in InitialState]
RootBelongsToRootGrp [axiom, in InitialState]
RWeq_dec [axiom, in SFSstate]
S
SCo [constructor, in ModelProperties]
SCu [constructor, in ModelProperties]
SecClassChanged [inductive, in ModelProperties]
SECLEV [definition, in SFSstate]
SECMATeq_dec [axiom, in SFSstate]
SecofrBelongsToAllGrp [axiom, in InitialState]
SecofrBelongsToSecAdmGrp [axiom, in InitialState]
SecureState [definition, in ModelProperties]
set [definition, in ListSet]
setACLdata [module]
set_add [definition, in ListSet]
Set_add1 [lemma, in ListFunctions]
Set_add2 [lemma, in ListFunctions]
set_add_elim [lemma, in ListSet]
set_add_intro [lemma, in ListSet]
set_add_intro1 [lemma, in ListSet]
set_add_intro2 [lemma, in ListSet]
set_add_not_empty [lemma, in ListSet]
set_diff [definition, in ListSet]
set_diff_elim1 [lemma, in ListSet]
set_diff_intro [lemma, in ListSet]
set_fold_left [definition, in ListSet]
set_fold_right [definition, in ListSet]
set_In [definition, in ListSet]
set_inter [definition, in ListSet]
set_inter_elim [lemma, in ListSet]
set_inter_elim1 [lemma, in ListSet]
set_inter_elim2 [lemma, in ListSet]
set_inter_intro [lemma, in ListSet]
set_In_dec [lemma, in ListSet]
set_map [definition, in ListSet]
set_mem [definition, in ListSet]
set_mem_complete1 [lemma, in ListSet]
set_mem_complete2 [lemma, in ListSet]
set_mem_correct1 [lemma, in ListSet]
set_mem_correct2 [lemma, in ListSet]
set_mem_ind [lemma, in ListSet]
set_power [definition, in ListSet]
set_prod [definition, in ListSet]
set_remove [definition, in ListSet]
Set_remove1 [lemma, in ListSet]
Set_remove2 [lemma, in ListFunctions]
set_union [definition, in ListSet]
Set_union1 [lemma, in ListFunctions]
Set_union2 [lemma, in ListFunctions]
set_union_elim [lemma, in ListSet]
set_union_intro [lemma, in ListSet]
set_union_intro1 [lemma, in ListSet]
set_union_intro2 [lemma, in ListSet]
SFSstate [module]
SimpleSecurity [definition, in ModelProperties]
SSCeq_dec [axiom, in SFSstate]
sscstat [inductive, in sscstat]
Sscstat [constructor, in SFSstate]
sscstat [module]
sscstatIsSecure [module]
SscstatOK [constructor, in sscstat]
SscstatPCP [lemma, in sscstatIsSecure]
SscstatPSP [lemma, in sscstatIsSecure]
SscstatPSS [lemma, in sscstatIsSecure]
StarProperty [definition, in ModelProperties]
StartPCP [tactic definition, in AuxiliaryLemmas]
StartPSP [tactic definition, in AuxiliaryLemmas]
StartPSS [tactic definition, in AuxiliaryLemmas]
Stat [constructor, in SFSstate]
stat [inductive, in stat]
stat [module]
statIsSecure [module]
StatOK [constructor, in stat]
StatPCP [lemma, in statIsSecure]
StatPSP [lemma, in statIsSecure]
StatPSS [lemma, in statIsSecure]
SUBeq_dec [axiom, in SFSstate]
SUBJECT [axiom, in SFSstate]
SysAllGrp [axiom, in InitialState]
SysGroups [axiom, in InitialState]
SysPrimaryGrp [axiom, in InitialState]
SysSubjectSC [axiom, in InitialState]
SysSubjectSCIsPARTFUNC [axiom, in InitialState]
T
take [definition, in ListFunctions]
TransFunc [inductive, in TransFunc]
TransFunc [module]
TwoImpLeft [lemma, in AuxiliaryLemmas]
TwoImpRight [lemma, in AuxiliaryLemmas]
U
UndefWhenRem [lemma, in FPF]
UniqNames [lemma, in AuxiliaryLemmas]
UNIX [constructor, in ModelProperties]
UNIXAttrChanged [inductive, in ModelProperties]
UNIXOwner [constructor, in DACandMAC]
Unlink [constructor, in SFSstate]
unlink [inductive, in unlink]
unlink [module]
unlinkIsSecure [module]
UnlinkOK [constructor, in unlink]
UnlinkPCP [lemma, in unlinkIsSecure]
UnlinkPSP [lemma, in unlinkIsSecure]
UnlinkPSS [lemma, in unlinkIsSecure]
unlink_acl [definition, in unlink]
unlink_directories [axiom, in SFSstate]
unlink_files [axiom, in SFSstate]
unlink_oSC [definition, in unlink]
UO [constructor, in ModelProperties]
UR [constructor, in ModelProperties]
UW [constructor, in ModelProperties]
W
WFSI1 [axiom, in ModelProperties]
WFSI2 [axiom, in ModelProperties]
WFSI3 [axiom, in ModelProperties]
WFSI4 [axiom, in ModelProperties]
WFSI5 [axiom, in ModelProperties]
WFSI6 [axiom, in ModelProperties]
WFSI7 [axiom, in ModelProperties]
WFSI8 [axiom, in ModelProperties]
WFSI9 [axiom, in ModelProperties]
write [inductive, in write]
WRITE [constructor, in SFSstate]
Write [constructor, in SFSstate]
write [module]
writeIsSecure [module]
WriteOK [constructor, in write]
WritePCP [lemma, in writeIsSecure]
WritePSP [lemma, in writeIsSecure]
WritePSS [lemma, in writeIsSecure]
write_files [axiom, in SFSstate]
_
_ [constructor, in read]
_ [constructor, in readdir]
_ [constructor, in sscstat]
Tactic Index
B
BreakSS [in AuxiliaryLemmas]
O
OpDontChangeStPSP [in AuxiliaryLemmas]
OpDontChangeStPSS [in AuxiliaryLemmas]
P
ProvePCP [in AuxiliaryLemmas]
S
StartPCP [in AuxiliaryLemmas]
StartPSP [in AuxiliaryLemmas]
StartPSS [in AuxiliaryLemmas]
Axiom Index
A
ACLeq_dec [in SFSstate]
B
BYTEeq_dec [in SFSstate]
C
CATEGORY [in SFSstate]
comp_mode [in stat]
create_directories [in SFSstate]
create_files [in SFSstate]
D
defaultState [in ModelLemmas]
G
GRPeq_dec [in SFSstate]
M
mkdir_directories [in SFSstate]
MyDir [in SFSstate]
O
OBJDeq_dec [in SFSstate]
OBJFeq_dec [in SFSstate]
OBJNAMEeq_dec [in SFSstate]
OSCeq_dec [in SFSstate]
R
rmdir_directories [in SFSstate]
root [in SFSstate]
RootBelongsToAllGrp [in InitialState]
RootBelongsToRootGrp [in InitialState]
RWeq_dec [in SFSstate]
S
SECMATeq_dec [in SFSstate]
SecofrBelongsToAllGrp [in InitialState]
SecofrBelongsToSecAdmGrp [in InitialState]
SSCeq_dec [in SFSstate]
SUBeq_dec [in SFSstate]
SUBJECT [in SFSstate]
SysAllGrp [in InitialState]
SysGroups [in InitialState]
SysPrimaryGrp [in InitialState]
SysSubjectSC [in InitialState]
SysSubjectSCIsPARTFUNC [in InitialState]
U
unlink_directories [in SFSstate]
unlink_files [in SFSstate]
W
WFSI1 [in ModelProperties]
WFSI2 [in ModelProperties]
WFSI3 [in ModelProperties]
WFSI4 [in ModelProperties]
WFSI5 [in ModelProperties]
WFSI6 [in ModelProperties]
WFSI7 [in ModelProperties]
WFSI8 [in ModelProperties]
WFSI9 [in ModelProperties]
write_files [in SFSstate]
Lemma Index
A
AclstatPCP [in aclstatIsSecure]
AclstatPSP [in aclstatIsSecure]
AclstatPSS [in aclstatIsSecure]
AddEq [in FPF]
AddEq1 [in FPF]
AddRemEq [in FPF]
AddUsrGrpToAclPCP [in addUsrGrpToAclIsSecure]
AddUsrGrpToAclPSP [in addUsrGrpToAclIsSecure]
AddUsrGrpToAclPSS [in addUsrGrpToAclIsSecure]
AllWaysIncluded [in ListFunctions]
Aux1 [in AuxiliaryLemmas]
B
BasicSecurityTheorem [in ModelLemmas]
C
ChmodPCP [in chmodIsSecure]
ChmodPSP [in chmodIsSecure]
ChmodPSS [in chmodIsSecure]
ChobjscPCP [in chobjscIsSecure]
ChobjscPSP [in chobjscIsSecure]
ChobjscPSS [in chobjscIsSecure]
Chobjsc_Corr [in AuxiliaryLemmas]
ChownPCP [in chownIsSecure]
ChownPSP [in chownIsSecure]
ChownPSS [in chownIsSecure]
ChsubscPCP [in chsubscIsSecure]
ChsubscPSP [in chsubscIsSecure]
ChsubscPSS [in chsubscIsSecure]
ChsubscPSS1 [in AuxiliaryLemmas]
Chsubsc_Corr [in AuxiliaryLemmas]
ClosePCP [in closeIsSecure]
ClosePSP [in closeIsSecure]
ClosePSS [in closeIsSecure]
Close_smCorr [in AuxiliaryLemmas]
Close_smCorr2 [in AuxiliaryLemmas]
Close_smCorr3 [in AuxiliaryLemmas]
CreatePCP [in createIsSecure]
CreatePSP [in createIsSecure]
CreatePSS [in createIsSecure]
D
DelUsrGrpFromAclPCP [in delUsrGrpFromAclIsSecure]
DelUsrGrpFromAclPSP [in delUsrGrpFromAclIsSecure]
DelUsrGrpFromAclPSS [in delUsrGrpFromAclIsSecure]
DIRCONTeq_dec [in SFSstate]
DOMFuncRel [in FPF]
DOMFuncRel2 [in FPF]
DOMFuncRel3 [in FPF]
DOMFuncRel4 [in FPF]
E
Eqfacl1 [in AuxiliaryLemmas]
Eqfacl2 [in AuxiliaryLemmas]
Eqfacl3 [in AuxiliaryLemmas]
Eqfacl4 [in AuxiliaryLemmas]
Eqfacl5 [in AuxiliaryLemmas]
EqfOSC1 [in AuxiliaryLemmas]
EqfOSC2 [in AuxiliaryLemmas]
EqfOSC3 [in AuxiliaryLemmas]
EqfOSC4 [in AuxiliaryLemmas]
EqfOSC5 [in AuxiliaryLemmas]
EqfOSC6 [in AuxiliaryLemmas]
EqfOSC7 [in AuxiliaryLemmas]
Eqfsecmat1 [in AuxiliaryLemmas]
Eqfsecmat2 [in AuxiliaryLemmas]
Eqfsecmat3 [in AuxiliaryLemmas]
EqfSSC1 [in AuxiliaryLemmas]
eq_scIMPLYle_sc [in AuxiliaryLemmas]
eq_scSym [in AuxiliaryLemmas]
F
FILECONTeq_dec [in SFSstate]
I
InDOMIsNotUndef [in FPF]
InDOMWhenAdd [in FPF]
InitialStateIsSecure [in ModelLemmas]
L
Listeq_dec [in ListFunctions]
M
MkdirPCP [in mkdirIsSecure]
MkdirPSP [in mkdirIsSecure]
MkdirPSS [in mkdirIsSecure]
N
NoDACChange [in AuxiliaryLemmas]
NoDACChange2 [in AuxiliaryLemmas]
NoMACObjChange [in AuxiliaryLemmas]
NoMACObjChange2 [in AuxiliaryLemmas]
NoMACSubChange [in AuxiliaryLemmas]
NoMACSubChange2 [in AuxiliaryLemmas]
NotInDOMIsUndef [in FPF]
NotInDOMIsUndef2 [in AuxiliaryLemmas]
NotInDOMIsUndef3 [in AuxiliaryLemmas]
O
OBJeq_dec [in SFSstate]
OBJTYPEeq_dec [in SFSstate]
OpenPCP [in openIsSecure]
OpenPSP [in openIsSecure]
OpenPSS [in openIsSecure]
Open_smCorr21 [in AuxiliaryLemmas]
Open_smCorr22 [in AuxiliaryLemmas]
Open_smCorr3 [in AuxiliaryLemmas]
Open_smCorr31 [in AuxiliaryLemmas]
Open_smCorr32 [in AuxiliaryLemmas]
OscstatPCP [in oscstatIsSecure]
OscstatPSP [in oscstatIsSecure]
OscstatPSS [in oscstatIsSecure]
OwnerClose_smCorr2 [in AuxiliaryLemmas]
OwnerClose_smCorr3 [in AuxiliaryLemmas]
Owner_ClosePCP [in owner_closeIsSecure]
Owner_ClosePSP [in owner_closeIsSecure]
Owner_ClosePSS [in owner_closeIsSecure]
P
Prodeq_dec [in ListFunctions]
R
ReaddirPCP [in readdirIsSecure]
ReaddirPSP [in readdirIsSecure]
ReaddirPSS [in readdirIsSecure]
ReadPCP [in readIsSecure]
ReadPSP [in readIsSecure]
ReadPSS [in readIsSecure]
ReadWriteImpRead [in AuxiliaryLemmas]
ReadWriteImpWrite [in AuxiliaryLemmas]
RemEq [in FPF]
RmdirPCP [in rmdirIsSecure]
RmdirPSP [in rmdirIsSecure]
RmdirPSS [in rmdirIsSecure]
S
Set_add1 [in ListFunctions]
Set_add2 [in ListFunctions]
set_add_elim [in ListSet]
set_add_intro [in ListSet]
set_add_intro1 [in ListSet]
set_add_intro2 [in ListSet]
set_add_not_empty [in ListSet]
set_diff_elim1 [in ListSet]
set_diff_intro [in ListSet]
set_inter_elim [in ListSet]
set_inter_elim1 [in ListSet]
set_inter_elim2 [in ListSet]
set_inter_intro [in ListSet]
set_In_dec [in ListSet]
set_mem_complete1 [in ListSet]
set_mem_complete2 [in ListSet]
set_mem_correct1 [in ListSet]
set_mem_correct2 [in ListSet]
set_mem_ind [in ListSet]
Set_remove1 [in ListSet]
Set_remove2 [in ListFunctions]
Set_union1 [in ListFunctions]
Set_union2 [in ListFunctions]
set_union_elim [in ListSet]
set_union_intro [in ListSet]
set_union_intro1 [in ListSet]
set_union_intro2 [in ListSet]
SscstatPCP [in sscstatIsSecure]
SscstatPSP [in sscstatIsSecure]
SscstatPSS [in sscstatIsSecure]
StatPCP [in statIsSecure]
StatPSP [in statIsSecure]
StatPSS [in statIsSecure]
T
TwoImpLeft [in AuxiliaryLemmas]
TwoImpRight [in AuxiliaryLemmas]
U
UndefWhenRem [in FPF]
UniqNames [in AuxiliaryLemmas]
UnlinkPCP [in unlinkIsSecure]
UnlinkPSP [in unlinkIsSecure]
UnlinkPSS [in unlinkIsSecure]
W
WritePCP [in writeIsSecure]
WritePSP [in writeIsSecure]
WritePSS [in writeIsSecure]
Constructor Index
A
ACL [in ModelProperties]
ACLGrp [in DACandMAC]
ACLOwner [in DACandMAC]
Aclstat [in SFSstate]
AclstatOK [in aclstat]
AddUsrGrpToAcl [in SFSstate]
addUsrGrpToAclOK [in addUsrGrpToAcl]
C
Categ [in ModelProperties]
Chmod [in SFSstate]
ChmodOK [in chmod]
Chobjsc [in SFSstate]
Chown [in SFSstate]
ChownOK [in chown]
chsobjscOK [in chobjsc]
Chsubsc [in SFSstate]
chsubscOK [in chsubsc]
Close [in SFSstate]
CloseOK [in close]
Create [in SFSstate]
CreateOK [in create]
D
DelUsrGrpFromAcl [in SFSstate]
delUsrGrpFromAclOK [in delUsrGrpFromAcl]
Directory [in SFSstate]
DoAclstat [in TransFunc]
DoAddUsrGrpToAcl [in TransFunc]
DoChmod [in TransFunc]
DoChobjsc [in TransFunc]
DoChown [in TransFunc]
DoChsubsc [in TransFunc]
DoClose [in TransFunc]
DoCreate [in TransFunc]
DoDelUsrGrpFromAcl [in TransFunc]
DoMkdir [in TransFunc]
DoOpen [in TransFunc]
DoOscstat [in TransFunc]
DoOwner_Close [in TransFunc]
DoRead [in TransFunc]
DoReaddir [in TransFunc]
DoRmdir [in TransFunc]
DoSscstat [in TransFunc]
DoStat [in TransFunc]
DoUnlink [in TransFunc]
DoWrite [in TransFunc]
F
File [in SFSstate]
G
GO [in ModelProperties]
GR [in ModelProperties]
Group [in ModelProperties]
GW [in ModelProperties]
I
IUO [in DACandMAC]
L
Level [in ModelProperties]
M
Mkdir [in SFSstate]
MkdirOK [in mkdir]
N
None [in mkdir]
None [in stat]
None [in owner_close]
None [in create]
None [in close]
None [in readdir]
None [in read]
None [in readdir]
None [in rmdir]
None [in read]
None [in sscstat]
None [in write]
None [in unlink]
O
Open [in SFSstate]
OpenRead [in open]
OpenWrite [in open]
Oscstat [in SFSstate]
OscstatOK [in oscstat]
Owner [in ModelProperties]
Owner_Close [in SFSstate]
Owner_CloseOK [in owner_close]
R
Read [in SFSstate]
READ [in SFSstate]
Readdir [in SFSstate]
ReaddirOK [in readdir]
ReadOK [in read]
Rmdir [in SFSstate]
RmdirOK [in rmdir]
S
SCo [in ModelProperties]
SCu [in ModelProperties]
Sscstat [in SFSstate]
SscstatOK [in sscstat]
Stat [in SFSstate]
StatOK [in stat]
U
UNIX [in ModelProperties]
UNIXOwner [in DACandMAC]
Unlink [in SFSstate]
UnlinkOK [in unlink]
UO [in ModelProperties]
UR [in ModelProperties]
UW [in ModelProperties]
W
WRITE [in SFSstate]
Write [in SFSstate]
WriteOK [in write]
_
_ [in read]
_ [in readdir]
_ [in sscstat]
Inductive Index
A
AclChanged [in ModelProperties]
aclstat [in aclstat]
addUsrGrpToAcl [in addUsrGrpToAcl]
C
chmod [in chmod]
chobjsc [in chobjsc]
chown [in chown]
chsubsc [in chsubsc]
close [in close]
create [in create]
D
DACCtrlAttrHaveChanged [in ModelProperties]
delUsrGrpFromAcl [in delUsrGrpFromAcl]
E
ExecuterIsOwner [in DACandMAC]
I
IsUNIXOwner [in DACandMAC]
M
MACObjCtrlAttrHaveChanged [in ModelProperties]
MACSubCtrlAttrHaveChanged [in ModelProperties]
mkdir [in mkdir]
MODE [in SFSstate]
O
OBJTYPE [in SFSstate]
open [in open]
Operation [in SFSstate]
oscstat [in oscstat]
owner_close [in owner_close]
R
read [in read]
readdir [in readdir]
rmdir [in rmdir]
S
SecClassChanged [in ModelProperties]
sscstat [in sscstat]
stat [in stat]
T
TransFunc [in TransFunc]
U
UNIXAttrChanged [in ModelProperties]
unlink [in unlink]
W
write [in write]
Definition Index
A
addUsrGrpToAcl_acl [in addUsrGrpToAcl]
C
ChangeGroupO [in setACLdata]
ChangeGroupR [in setACLdata]
ChangeGroupW [in setACLdata]
ChangeUserR [in setACLdata]
ChangeUserW [in setACLdata]
chmod_acl [in chmod]
chobjsc_SC [in chobjsc]
chown_acl [in chown]
chsubsc_SC [in chsubsc]
close_sm [in close]
ControlProperty [in ModelProperties]
create_acl [in create]
create_oSC [in create]
D
DACSecureState [in ModelProperties]
delUsrGrpFromAcl_acl [in delUsrGrpFromAcl]
DIRCONT [in SFSstate]
DOM [in FPF]
domacl [in SFSstate]
domd [in SFSstate]
domf [in SFSstate]
domOSC [in SFSstate]
domsecmat [in SFSstate]
domSSC [in SFSstate]
E
empty_set [in ListSet]
eq_sc [in SFSstate]
F
facl [in SFSstate]
fdirs [in SFSstate]
ffiles [in SFSstate]
FILECONT [in SFSstate]
fOSC [in SFSstate]
front [in ListFunctions]
fsecmat [in SFSstate]
fSSC [in SFSstate]
FuncPre1 [in ModelProperties]
FuncPre2 [in ModelProperties]
FuncPre3 [in ModelProperties]
FuncPre4 [in ModelProperties]
FuncPre5 [in ModelProperties]
FuncPre6 [in ModelProperties]
FuncPre7 [in ModelProperties]
G
GeneralSecureState [in ModelLemmas]
I
Included [in ListFunctions]
InFileSystem [in DACandMAC]
InitState [in InitialState]
IsEmpty [in ListFunctions]
IsPARTFUNC [in FPF]
L
last [in ListFunctions]
le_sc [in SFSstate]
M
mkdir_acl [in mkdir]
mkdir_oSC [in mkdir]
N
NEWDIR [in mkdir]
NEWFILE [in create]
NEWRW [in close]
NEWRWOC [in owner_close]
O
OBJECT [in SFSstate]
ObjName [in SFSstate]
ObjType [in SFSstate]
open_sm [in open]
ownerclose_sm [in owner_close]
P
PARTFUNC [in FPF]
PreDACRead [in DACandMAC]
PreDACWrite [in DACandMAC]
PreMAC [in DACandMAC]
PreservesControlProp [in ModelProperties]
PreStarPropRead [in DACandMAC]
PreStarPropWrite [in DACandMAC]
R
RAN [in FPF]
ransecmat [in SFSstate]
rmdir_acl [in rmdir]
rmdir_oSC [in rmdir]
S
SECLEV [in SFSstate]
SecureState [in ModelProperties]
set [in ListSet]
set_add [in ListSet]
set_diff [in ListSet]
set_fold_left [in ListSet]
set_fold_right [in ListSet]
set_In [in ListSet]
set_inter [in ListSet]
set_map [in ListSet]
set_mem [in ListSet]
set_power [in ListSet]
set_prod [in ListSet]
set_remove [in ListSet]
set_union [in ListSet]
SimpleSecurity [in ModelProperties]
StarProperty [in ModelProperties]
T
take [in ListFunctions]
U
unlink_acl [in unlink]
unlink_oSC [in unlink]
Module Index
A
aclstat
aclstatIsSecure
addUsrGrpToAcl
addUsrGrpToAclIsSecure
AuxiliaryLemmas
C
chmod
chmodIsSecure
chobjsc
chobjscIsSecure
chown
chownIsSecure
chsubsc
chsubscIsSecure
close
closeIsSecure
create
createIsSecure
D
DACandMAC
delUsrGrpFromAcl
delUsrGrpFromAclIsSecure
F
FPF
I
InitialState
L
ListFunctions
ListSet
M
mkdir
mkdirIsSecure
ModelLemmas
ModelProperties
O
open
openIsSecure
oscstat
oscstatIsSecure
owner_close
owner_closeIsSecure
R
read
readdir
readdirIsSecure
readIsSecure
rmdir
rmdirIsSecure
S
setACLdata
SFSstate
sscstat
sscstatIsSecure
stat
statIsSecure
T
TransFunc
U
unlink
unlinkIsSecure
W
write
writeIsSecure
| Global Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(475 entries) |
| Tactic Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(7 entries) |
| Axiom Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(42 entries) |
| Lemma Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(153 entries) |
| Constructor Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(99 entries) |
| Inductive Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(32 entries) |
| Definition Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(91 entries) |
| Module Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(51 entries) |
This page has been generated by coqdoc