Skip to content

Commit

Permalink
Added teams, internal/external users (FINMA 50).
Browse files Browse the repository at this point in the history
  • Loading branch information
vinahradau authored May 31, 2020
1 parent 595c5c2 commit dbd4a88
Showing 1 changed file with 152 additions and 37 deletions.
189 changes: 152 additions & 37 deletions jaza/CIDFINMA_spec_Z_jaza_case_2_1.txt
Original file line number Diff line number Diff line change
Expand Up @@ -6,107 +6,203 @@ Classification, storage and bulk access of CID data:
- customer name classified as DIRECT CID data (ImplementDataClassification operation);
- vip customer flag classified as NONCID data (ImplementDataClassification operation);
- CID and NONCID data stored on a node in Switzerland (AddNodeData operation);
- USER1 is given access rights for cid bulk access (AddUserAccessRights operation);
- USER2 is given access rights for bulk access (non-CID) (AddUserAccessRights operation);
- USER1 is added to team ENTITY2 and external users (S. AddUser and AddExternalUser operations);
- USER2 is added to team ENTITY2 and internal users (S. AddUser and AddExternalUser operations);
- USER1 is given access rights for cid bulk access (S. AddUserAccessRights operation);
- USER2 is given access rights for bulk access (non-CID) (S. AddUserAccessRights operation);
- USER1 in Switzerland with CID bulk access rights successfully accesses bulk data, CID bulk log record created (S. cidBulkAccess and contentOutput! variables in AccessBulk operation);
- USER1 from outside Switzerland with bulk access rights: no accesses to bulk data (no solution provided by jaza in AccessBulk operation);
- USER2 in Switzerland with bulk access (non-CID) rights: no accesses to bulk data (no solution provided by jaza in AccessBulk operation);
- USER2 from outside Switzerland with bulk access (non-CID) rights: no accesses to bulk data (no solution provided by jaza in AccessBulk operation);
- USER3 without access rights: no access (no solution provided by jaza in AccessBulk operation).


JAZA> load CIDFINMA_spec_Z.zed
Loading 'CIDFINMA_spec_Z.zed' ...
Added 24 definitions.
Added 28 definitions.
JAZA> do InitDomain
\lblot cidBulkAccess'==\{\}, cidStoringNodesIds'==\{\},
classificationMetadata'==\{\}, dataClassification'==\{\},
dataOwner'==\{\}, dataOwnerMetadata'==\{\},
nodeContentsMetadata'==\{\}, nodeCountry'==GERMANY,
nodeDataCategories'==\{\}, nodeDataContents'==\{\}, nodeId'==NODE1,
nodeMetadata'==\{\}, roles'==\{\}, rolesRoles'==\{\},
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{\}, classificationMetadata'==\{\},
dataClassification'==\{\}, dataOwner'==\{\},
dataOwnerMetadata'==\{\}, externalUsers'==\{\},
internalUsers'==\{\}, nodeContentsMetadata'==\{\},
nodeCountry'==GERMANY, nodeDataCategories'==\{\},
nodeDataContents'==\{\}, nodeId'==NODE1, nodeMetadata'==\{\},
roles'==\{\}, rolesRoles'==\{\}, teams'==\{\}, teamsTeams'==\{\},
userAccessRigths'==\{\} \rblot
JAZA> ; ImplementDataClassification
Input metadata? = CUSTOMERNAME
Input dataOwnerInput? = ENTITY1
Input dataCategory? = DIRECT
\lblot cidBulkAccess'==\{\}, cidStoringNodesIds'==\{\},
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{\},
classificationMetadata'==\{CUSTOMERNAME\},
dataClassification'==\{(CUSTOMERNAME, DIRECT)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME\}, nodeContentsMetadata'==\{\},
dataOwnerMetadata'==\{CUSTOMERNAME\}, externalUsers'==\{\},
internalUsers'==\{\}, nodeContentsMetadata'==\{\},
nodeCountry'==GERMANY, nodeDataCategories'==\{\},
nodeDataContents'==\{\}, nodeId'==NODE1, nodeMetadata'==\{\},
roles'==\{\}, rolesRoles'==\{\}, userAccessRigths'==\{\} \rblot
JAZA>
JAZA>
JAZA>
roles'==\{\}, rolesRoles'==\{\}, teams'==\{\}, teamsTeams'==\{\},
userAccessRigths'==\{\} \rblot
JAZA> ; ImplementDataClassification
Input metadata? = ISVIPCUSTOMER
Input dataOwnerInput? = ENTITY1
Input dataCategory? = NONCID
\lblot cidBulkAccess'==\{\}, cidStoringNodesIds'==\{\},
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{\},
nodeContentsMetadata'==\{\}, nodeCountry'==GERMANY,
nodeDataCategories'==\{\}, nodeDataContents'==\{\}, nodeId'==NODE1,
nodeMetadata'==\{\}, roles'==\{\}, rolesRoles'==\{\},
userAccessRigths'==\{\} \rblot
JAZA>
JAZA>
nodeMetadata'==\{\}, roles'==\{\}, rolesRoles'==\{\}, teams'==\{\},
teamsTeams'==\{\}, userAccessRigths'==\{\} \rblot
JAZA> ; AddNodeData
Input nodeIdInput? = NODE1
Input nodeCountryInput? = SWITZERLAND
Input nodeMetadataInput? = CUSTOMERNAME
Input nodeDataContentInput? = MUSTERMANN
\lblot cidBulkAccess'==\{\}, cidStoringNodesIds'==\{NODE1\},
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{NODE1\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{\},
nodeContentsMetadata'==\{CUSTOMERNAME\}, nodeCountry'==SWITZERLAND,
nodeDataCategories'==\{(CUSTOMERNAME, DIRECT)\},
nodeDataContents'==\{(CUSTOMERNAME, MUSTERMANN)\}, nodeId'==NODE1,
nodeMetadata'==\{CUSTOMERNAME\}, roles'==\{\}, rolesRoles'==\{\},
userAccessRigths'==\{\} \rblot
JAZA>
JAZA>
teams'==\{\}, teamsTeams'==\{\}, userAccessRigths'==\{\} \rblot
JAZA> ; AddNodeData
Input nodeIdInput? = NODE1
Input nodeCountryInput? = SWITZERLAND
Input nodeMetadataInput? = ISVIPCUSTOMER
Input nodeDataContentInput? = YES
\lblot cidBulkAccess'==\{\}, cidStoringNodesIds'==\{NODE1\},
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{NODE1\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{\},
nodeContentsMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
nodeCountry'==SWITZERLAND,
nodeDataCategories'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
nodeDataContents'==\{(CUSTOMERNAME, MUSTERMANN),
(ISVIPCUSTOMER, YES)\},
nodeId'==NODE1, nodeMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
roles'==\{\}, rolesRoles'==\{\}, userAccessRigths'==\{\} \rblot
roles'==\{\}, rolesRoles'==\{\}, teams'==\{\}, teamsTeams'==\{\},
userAccessRigths'==\{\} \rblot
JAZA>
JAZA>
JAZA>
JAZA> ; AddUser
Input user? = USER1
Input entity? = ENTITY2
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{NODE1\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{\},
nodeContentsMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
nodeCountry'==SWITZERLAND,
nodeDataCategories'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
nodeDataContents'==\{(CUSTOMERNAME, MUSTERMANN),
(ISVIPCUSTOMER, YES)\},
nodeId'==NODE1, nodeMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
roles'==\{\}, rolesRoles'==\{\}, teams'==\{(ENTITY2, USER1)\},
teamsTeams'==\{ENTITY2\}, userAccessRigths'==\{\} \rblot
JAZA> ; AddInternalUser
Input user? = USER1
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{NODE1\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{USER1\},
nodeContentsMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
nodeCountry'==SWITZERLAND,
nodeDataCategories'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
nodeDataContents'==\{(CUSTOMERNAME, MUSTERMANN),
(ISVIPCUSTOMER, YES)\},
nodeId'==NODE1, nodeMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
roles'==\{\}, rolesRoles'==\{\}, teams'==\{(ENTITY2, USER1)\},
teamsTeams'==\{ENTITY2\}, userAccessRigths'==\{\} \rblot
JAZA>
JAZA> ; AddUserAccessRights
JAZA>
JAZA>
JAZA> ; AddUser
Input user? = USER2
Input entity? = ENTITY2
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{NODE1\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{USER1\},
nodeContentsMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
nodeCountry'==SWITZERLAND,
nodeDataCategories'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
nodeDataContents'==\{(CUSTOMERNAME, MUSTERMANN),
(ISVIPCUSTOMER, YES)\},
nodeId'==NODE1, nodeMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
roles'==\{\}, rolesRoles'==\{\},
teams'==\{(ENTITY2, USER1), (ENTITY2, USER2)\},
teamsTeams'==\{ENTITY2\}, userAccessRigths'==\{\} \rblot
JAZA>
JAZA>
JAZA>
JAZA> ; AddInternalUser
Input user? = USER2
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{NODE1\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{USER1, USER2\},
nodeContentsMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
nodeCountry'==SWITZERLAND,
nodeDataCategories'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
nodeDataContents'==\{(CUSTOMERNAME, MUSTERMANN),
(ISVIPCUSTOMER, YES)\},
nodeId'==NODE1, nodeMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
roles'==\{\}, rolesRoles'==\{\},
teams'==\{(ENTITY2, USER1), (ENTITY2, USER2)\},
teamsTeams'==\{ENTITY2\}, userAccessRigths'==\{\} \rblot
JAZA>
JAZA>
JAZA>
JAZA> ; AddUserAccessRight
Input user? = USER1
Input role? = ROLEBULKCID
\lblot cidBulkAccess'==\{\}, cidStoringNodesIds'==\{NODE1\},
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{NODE1\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{USER1, USER2\},
nodeContentsMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
nodeCountry'==SWITZERLAND,
nodeDataCategories'==\{(CUSTOMERNAME, DIRECT),
Expand All @@ -115,18 +211,20 @@ JAZA> ; AddUserAccessRights
(ISVIPCUSTOMER, YES)\},
nodeId'==NODE1, nodeMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
roles'==\{\}, rolesRoles'==\{\},
teams'==\{(ENTITY2, USER1), (ENTITY2, USER2)\},
teamsTeams'==\{ENTITY2\},
userAccessRigths'==\{(USER1, ROLEBULKCID)\} \rblot
JAZA>
JAZA>
JAZA> ; AddUserAccessRights
JAZA> ; AddUserAccessRight
Input user? = USER2
Input role? = ROLEBULK
\lblot cidBulkAccess'==\{\}, cidStoringNodesIds'==\{NODE1\},
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{NODE1\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{USER1, USER2\},
nodeContentsMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
nodeCountry'==SWITZERLAND,
nodeDataCategories'==\{(CUSTOMERNAME, DIRECT),
Expand All @@ -135,23 +233,26 @@ JAZA> ; AddUserAccessRights
(ISVIPCUSTOMER, YES)\},
nodeId'==NODE1, nodeMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
roles'==\{\}, rolesRoles'==\{\},
teams'==\{(ENTITY2, USER1), (ENTITY2, USER2)\},
teamsTeams'==\{ENTITY2\},
userAccessRigths'==\{(USER1, ROLEBULKCID),
(USER2, ROLEBULK)\} \rblot
JAZA>
JAZA>
JAZA>
JAZA>
JAZA> ; AccessBulk
Input user? = USER1
Input nodeId? = NODE1
Input userCountry? = SWITZERLAND
\lblot cidBulkAccess'==\{(USER1, NODE1)\}, cidStoringNodesIds'==\{NODE1\},
\lblot cidBulkAccess'==\{\}, cidBulkAccessUsers'==\{\},
cidStoringNodesIds'==\{NODE1\},
classificationMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
contentOutput!==\{MUSTERMANN, YES\},
dataClassification'==\{(CUSTOMERNAME, DIRECT),
(ISVIPCUSTOMER, NONCID)\},
dataOwner'==\{(CUSTOMERNAME, ENTITY1), (ISVIPCUSTOMER, ENTITY1)\},
dataOwnerMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
externalUsers'==\{\}, internalUsers'==\{USER1, USER2\},
nodeContentsMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
nodeCountry'==SWITZERLAND,
nodeDataCategories'==\{(CUSTOMERNAME, DIRECT),
Expand All @@ -160,33 +261,47 @@ JAZA> ; AccessBulk
(ISVIPCUSTOMER, YES)\},
nodeId'==NODE1, nodeMetadata'==\{CUSTOMERNAME, ISVIPCUSTOMER\},
roles'==\{\}, rolesRoles'==\{\},
teams'==\{(ENTITY2, USER1), (ENTITY2, USER2)\},
teamsTeams'==\{ENTITY2\},
userAccessRigths'==\{(USER1, ROLEBULKCID),
(USER2, ROLEBULK)\} \rblot
JAZA>
JAZA>
JAZA>
JAZA> ; AccessBulk
Input user? = USER1
Input nodeId? = NODE1
Input userCountry? = USA
No solutions
JAZA>
JAZA> ; AccessBulk
No current state
JAZA> undo
undone operation: AccessBulk
JAZA>
JAZA>
JAZA>
JAZA> ; AccessBulk
Input user? = USER2
Input nodeId? = NODE1
Input userCountry? = SWITZERLAND
No solutions
JAZA>
JAZA>
JAZA>
JAZA> undo
undone operation: AccessBulk
JAZA> USER2
Unknown/illegal command.
JAZA>
JAZA> ; AccessBulk
Input user? = USER2
Input user? = USER1
Input nodeId? = NODE1
Input userCountry? = USA
No solutions
JAZA>
JAZA>
JAZA>
JAZA> undo
undone operation: AccessBulk
JAZA>
Expand All @@ -196,4 +311,4 @@ JAZA> ; AccessBulk
Input nodeId? = NODE1
Input userCountry? = SWITZERLAND
No solutions
JAZA>
JAZA>

0 comments on commit dbd4a88

Please sign in to comment.