Dependencies:FIA_UID.1 timing of identification
FIA_UID.2 User identification before any action
Dependencies:No dependencies
FIA_UAU.3 Unforgeable authentication
Dependencies:No dependencies
FIA_UAU.3.1 The Teaclave access control module shall prevent use of authentication data that has been forged by any user of the Teaclave access control module. (This requirement is already covered by assumption, so it is not formalized.)
FIA_UAU.3.2 The Teaclave access control module shall prevent use of authentication data that has been copied from any other user of the Teaclave access control module. (This requirement is already covered by assumption, so it is not formalized.)
FIA_USB.1 User-subject binding
Dependencies:FIA_ATD.1 User attribute definition
FIA_USB.1.1 The Teaclave access control module shall associate the following user security attributes with subjects acting on the behalf of that user: UsrId.
FIA_USB.1.2 The Teaclave access control module shall enforce the following rules on the initial association of user security attributes with subjects acting on the behalf of users: UsrId is in the participants of subjects.
FIA_USB.1.3 The Teaclave access control module shall enforce the following rules governing changes to the user security attributes associated with subjects acting on the behalf of users: None.
FIA_ATD.1 User attribute definition
Dependencies:No dependencies
FDP_ACC.1 Subset access control
Dependencies:FDP_ACF.1 Security attribute based access control
FDP_ACF.1 Security attribute based access control
Dependencies:FDP_ACC.1 Subset access control;
FMT_MSA.3:Static attribute initialisation
FDP_ACF.1.1 The Teaclave access control module shall enforce the Teaclave Subset access control SFP to objects based on the following:
subject attributes: task_participant; UsrId
object attributes: function_owner; data_owner.
FDP_ACF.1.2 The TSF shall enforce the following rules to determine if an operation among controlled subjects and controlled objects is allowed:
task_access_data is allowed if data_owner is the subset of task_participant;
task_access_function is allowed if function_owner is the subset of task_participant;
user_access_data is allowed if UsrId is in data_owner;
user_access_function is allowed if UsrId is in function_owner.
FDP_ACF.1.3 The TSF shall explicitly authorize access of subjects to objects based on the following additional rules: NONE.
FDP_ACF.1.4 The TSF shall explicitly deny access of subjects to objects based on the following additional rules: NONE.
FMT_MSA.3 Static attribute initialization
Dependencies:FMT_MSA.1 Management of security attributes;
FMT_SMR.1 Security roles
FMT_MSA.3.1 The Teaclave access control shall enforce the Teaclave Subset access control SFP to provide permissive default values for security attributes that are used to enforce the SFP.
FMT_MSA.3.2 The TSF shall not allow the Users to specify alternative initial values to override the default values when an object or information is created.
FMT_MSA.1 Management of security attributes
Dependencies:FDP_IFC.1 Subset information flow control;
FMT_SMR.1 Security roles;
FMT_SMF.1 Specification of Management Functions
FMT_SMR.1 Security roles
Dependencies:FIA_UID.1 Timing of identification
FMT_SMR.1.1 The Teaclave access control module shall maintain the roles: User.
FMT_SMR.1.2 The Teaclave access control module shall be able to associate users with roles.
FMT_SMF.1 Specification of Management Functions
Dependencies:No dependencies
Each security functional requirement listed above is formalized and located in different files. For more information, please refer to access control module introduction
.