Library FSSecModel.ModelLemmas

Library FSSecModel.writeIsSecure

Library FSSecModel.unlinkIsSecure

Library FSSecModel.statIsSecure

Library FSSecModel.sscstatIsSecure

Library FSSecModel.rmdirIsSecure

Library FSSecModel.readIsSecure

Library FSSecModel.readdirIsSecure

Library FSSecModel.owner_closeIsSecure

Library FSSecModel.oscstatIsSecure

Library FSSecModel.openIsSecure

Library FSSecModel.mkdirIsSecure

Library FSSecModel.delUsrGrpFromAclIsSecure

Library FSSecModel.createIsSecure

Library FSSecModel.closeIsSecure

Library FSSecModel.chsubscIsSecure

Library FSSecModel.chownIsSecure

Library FSSecModel.chobjscIsSecure

Library FSSecModel.chmodIsSecure

Library FSSecModel.addUsrGrpToAclIsSecure

Library FSSecModel.aclstatIsSecure

Library FSSecModel.AuxiliaryLemmas

Library FSSecModel.ModelProperties

Library FSSecModel.TransFunc

Library FSSecModel.delUsrGrpFromAcl

Library FSSecModel.read

Library FSSecModel.aclstat

Library FSSecModel.addUsrGrpToAcl

Library FSSecModel.chobjsc

Library FSSecModel.chown

Library FSSecModel.chsubsc

Library FSSecModel.close

Library FSSecModel.open

Library FSSecModel.oscstat

Library FSSecModel.owner_close

Library FSSecModel.readdir

Library FSSecModel.rmdir

Library FSSecModel.stat

Library FSSecModel.unlink

Library FSSecModel.write

Library FSSecModel.chmod

Library FSSecModel.create

Library FSSecModel.mkdir

Library FSSecModel.DACandMAC

Library FSSecModel.setACLdata

Library FSSecModel.sscstat

Library FSSecModel.InitialState

Library FSSecModel.SFSstate

Library FSSecModel.ListFunctions

Library FSSecModel.ListSet