aclstat/
aclstatIsSecure/
addUsrGrpToAcl/
addUsrGrpToAclIsSecure/
AuxiliaryLemmas/
chmod/
chmodIsSecure/
chobjsc/
chobjscIsSecure/
chown/
chownIsSecure/
chsubsc/
chsubscIsSecure/
close/
closeIsSecure/
create/
createIsSecure/
DACandMAC/
delUsrGrpFromAcl/
delUsrGrpFromAclIsSecure/
InitialState/
ListFunctions/
ListSet/
mkdir/
mkdirIsSecure/
ModelLemmas/
ModelProperties/
open/
openIsSecure/
oscstat/
oscstatIsSecure/
owner_close/
owner_closeIsSecure/
read/
readdir/
readdirIsSecure/
readIsSecure/
rmdir/
rmdirIsSecure/
setACLdata/
SFSstate/
sscstat/
sscstatIsSecure/
stat/
statIsSecure/
TransFunc/
unlink/
unlinkIsSecure/
write/
writeIsSecure/