CIDFINMA_spec_Z.zed

Client Identifying Data (CID) Requirements Specification for banks in Switzerland 
Language: Z Notation
Developed By Serge (Siarhei Vinahradau, vinahradau@yahoo.de
Specification, further referred to as FINMA:
https://www.finma.ch/de/~/media/finma/dokumente/rundschreiben-archiv/finma-rs200821---30-06-2017.pdf

Specification requirements:
-CID data classification (FINMA 10*)
	DATACATEGORY
	CIDCATEGORIES
	METADATA
- CID data owner (FINMA 13*)
	ENTITY
	DOMAIN
- all nodes with CID data stored should be recorded (FINMA 15*)
	CIDSTORINGNODESAUDITLOG
- CID protection risks are country specific (FINMA 20*)
	COUNTRY
- no node outside Switzerland should have unprotected CID data stored (FINMA 20*)
	CONTENT
	NODE
	AddNodeData
- CID data accessed by users from outside Switzerland has to be protected (FINMA 20*)
	AccesNodeData
- role and function based authorisation system in place (FINMA 22*)
	ROLE
	USER
	DOMAIN
- List of users with bulk CID access (FINMA 34*)
	BulkCIDAccessUsersList
- logs for bulk CID access (FINMA 40*)
	CIDBULKLOG
- an internal employee has to be responsible for the compliance of outsourced CID activities (FINMA 50*)
	DOMAIN
	USER
	AddUser
	AddInternalUser
	AddExternalUser
\begin{zsection}	 \SECTION Specification \parents~standard\_toolkit , zeves\_toolkit
\end{zsection}

\begin{zed}DATACATEGORY ::= DIRECT | INDIRECT | POTENTIALLYDIRECT | PROTECTED | NONCID
\end{zed}

\begin{zed}CIDCATEGORIES == \{ DIRECT , INDIRECT , POTENTIALLYDIRECT \}
\end{zed}

\begin{zed}COUNTRY ::= SWITZERLAND | UK | USA | GERMANY
\end{zed}

\begin{zed}METADATA ::= CUSTOMERNAME | CUSTOMERADDRESS | ISVIPCUSTOMER
\end{zed}

\begin{zed}CONTENT ::= MUSTERMANN | SEESTRASSE | YES | NO | XXXXX
\end{zed}

\begin{zed}ENTITY ::= ENTITY1 | ENTITY2 | ENTITY3
\end{zed}

\begin{zed}USER ::= USER1 | USER2 | USER3
\end{zed}

\begin{zed}ROLE ::= ROLEGUICIDUSER | ROLEGUIUSER | ROLEBULKCID | ROLEBULK | ROLE1
\end{zed}

\begin{zed}CIDROLES == \{ ROLEGUICIDUSER , ROLEBULKCID \}
\end{zed}

\begin{zed}NODEID ::= NODE1 | NODE2 | NODE3
\end{zed}


\begin{schema}{NODE}
 nodeId : NODEID \\
 nodeCountry : COUNTRY \\
 nodeDataCategories : METADATA \pfun DATACATEGORY \\
 nodeDataContents : METADATA \pfun CONTENT \\
 nodeMetadata : \power METADATA \\
 nodeContentsMetadata : \power METADATA 
\where
 nodeCountry = SWITZERLAND \lor ( \forall c : \ran nodeDataCategories @ c \notin CIDCATEGORIES ) \\
 \dom nodeDataContents \subseteq \dom nodeDataCategories \\
 nodeMetadata = \dom nodeDataCategories \\
 nodeContentsMetadata = \dom nodeDataContents
\end{schema}


\begin{schema}{DOMAIN}
 dataClassification : METADATA \pfun DATACATEGORY \\
 dataOwner : METADATA \pfun ENTITY \\
 roles : ROLE \rel METADATA \\
 userAccessRigths : USER \rel ROLE \\
 teams : ENTITY \rel USER \\
 internalUsers : \power USER \\
 externalUsers : \power USER \\
 classificationMetadata : \power METADATA \\
 dataOwnerMetadata : \power METADATA \\
 rolesRoles : \power ROLE \\
 teamsTeams : \power ENTITY 
\where
 \forall u : USER @ \lnot ( u \in internalUsers \land u \in externalUsers ) \\
 \forall u : \dom userAccessRigths @ u \in \ran teams \\
 \forall u : \dom userAccessRigths @ u \in internalUsers \lor u \in externalUsers \\
 \forall u : externalUsers @ \lnot ( userAccessRigths \limg \{ u \} \rimg \cap CIDROLES \neq \emptyset \land teams \limg \dom ( teams \rres \{ u \} ) \rimg \cap internalUsers =~\emptyset ) \\
 classificationMetadata = \dom dataClassification \\
 dataOwnerMetadata = \dom dataOwner \\
 rolesRoles = \dom roles \\
 \dom dataClassification \subseteq \dom dataOwner \\
 teamsTeams = \dom teams \\
 \# ( \dom dataClassification ) < 6 \\
 \# ( \dom dataOwner ) < 6
\end{schema}


\begin{schema}{CIDSTORINGNODESAUDITLOG}
 cidStoringNodesIds : \power NODEID \\
 NODE
\where
 \# ( cidStoringNodesIds ) < 6\\
 \forall cidDataCategory : \ran nodeDataCategories @ cidDataCategory \in CIDCATEGORIES \implies nodeId \in cidStoringNodesIds
\end{schema}


\begin{schema}{CIDBULKLOG}
 cidBulkAccess : USER \rel NODEID \\
 cidBulkAccessUsers : \power USER 
\where
 cidBulkAccessUsers = \dom cidBulkAccess \\
 \# ( cidBulkAccess ) < 6
\end{schema}


\begin{schema}{InitDomain}
 DOMAIN~' \\
 NODE~' \\
 CIDSTORINGNODESAUDITLOG~' \\
 CIDBULKLOG~' 
\where
 dataOwnerMetadata' =~\emptyset \\
 classificationMetadata' =~\emptyset \\
 userAccessRigths' =~\emptyset \\
 teams' =~\emptyset \\
 internalUsers' =~\emptyset \\
 externalUsers' =~\emptyset \\
 nodeMetadata' =~\emptyset \\
 cidStoringNodesIds' =~\emptyset \\
 nodeId' = NODE1 \\
 cidBulkAccess' =~\emptyset
\end{schema}


\begin{schema}{AddRole}
 \Delta DOMAIN \\
 role? : ROLE \\
 metadata? : METADATA 
\where
 roles' = roles \cup \{ ( role? , metadata? ) \} \\
 dataClassification' = dataClassification \\
 teams' = teams \\
 internalUsers' = internalUsers \\
 externalUsers' = externalUsers \\
 dataOwner' = dataOwner \\
 userAccessRigths' = userAccessRigths
\end{schema}


\begin{schema}{AddUser}
 \Delta DOMAIN \\
 user? : USER \\
 entity? : ENTITY 
\where
 teams' = teams \cup \{ ( entity? , user? ) \} \\
 userAccessRigths' = userAccessRigths \\
 roles' = roles \\
 internalUsers' = internalUsers \\
 externalUsers' = externalUsers \\
 dataClassification' = dataClassification \\
 dataOwner' = dataOwner
\end{schema}


\begin{schema}{AddExternalUser}
 \Delta DOMAIN \\
 user? : USER 
\where
 externalUsers' = externalUsers \cup \{ user? \} \\
 internalUsers' = internalUsers \\
 teams' = teams \\
 userAccessRigths' = userAccessRigths \\
 roles' = roles \\
 dataClassification' = dataClassification \\
 dataOwner' = dataOwner
\end{schema}


\begin{schema}{AddInternalUser}
 \Delta DOMAIN \\
 user? : USER 
\where
 internalUsers' = internalUsers \cup \{ user? \} \\
 externalUsers' = externalUsers \\
 teams' = teams \\
 userAccessRigths' = userAccessRigths \\
 roles' = roles \\
 dataClassification' = dataClassification \\
 dataOwner' = dataOwner
\end{schema}


\begin{schema}{AddUserAccessRight}
 \Delta DOMAIN \\
 user? : USER \\
 role? : ROLE 
\where
 userAccessRigths' = userAccessRigths \cup \{ ( user? , role? ) \} \\
 teams' = teams \\
 internalUsers' = internalUsers \\
 externalUsers' = externalUsers \\
 roles' = roles \\
 dataClassification' = dataClassification \\
 dataOwner' = dataOwner
\end{schema}


\begin{schema}{RemoveUserAccessRight}
 \Delta DOMAIN \\
 user? : USER \\
 role? : ROLE 
\where
 userAccessRigths' = userAccessRigths \setminus \{ ( user? , role? ) \} \\
 roles' = roles \\
 teams' = teams \\
 internalUsers' = internalUsers \\
 externalUsers' = externalUsers \\
 dataClassification' = dataClassification \\
 dataOwner' = dataOwner
\end{schema}


\begin{schema}{AddNodeData}
 \Delta NODE \\
 \Delta CIDSTORINGNODESAUDITLOG \\
 \Xi DOMAIN \\
 nodeIdInput? : NODEID \\
 nodeCountryInput? : COUNTRY \\
 nodeMetadataInput? : METADATA \\
 nodeDataContentInput? : CONTENT 
\where
 nodeCountry' = nodeCountryInput? \land nodeId' = nodeIdInput? \land ( ( nodeCountryInput? = SWITZERLAND \land ( dataClassification~nodeMetadataInput? ) \in CIDCATEGORIES \land cidStoringNodesIds' = cidStoringNodesIds \cup \{ nodeIdInput? \} \land nodeDataContents' = nodeDataContents \oplus \{ nodeMetadataInput? \mapsto nodeDataContentInput? \} \land nodeDataCategories' = nodeDataCategories \oplus \{ nodeMetadataInput? \mapsto ( dataClassification~nodeMetadataInput? ) \} ) \lor ( ( dataClassification~nodeMetadataInput? ) \notin CIDCATEGORIES \land cidStoringNodesIds' = cidStoringNodesIds \land nodeDataContents' = nodeDataContents \oplus \{ nodeMetadataInput? \mapsto nodeDataContentInput? \} \land nodeDataCategories' = nodeDataCategories \oplus \{ nodeMetadataInput? \mapsto ( dataClassification~nodeMetadataInput? ) \} ) \lor ( nodeCountryInput? \neq SWITZERLAND \land ( dataClassification~nodeMetadataInput? ) \in CIDCATEGORIES \land cidStoringNodesIds' = cidStoringNodesIds \land nodeDataContents' = nodeDataContents \oplus \{ nodeMetadataInput? \mapsto XXXXX \} \land nodeDataCategories' = nodeDataCategories \oplus \{ nodeMetadataInput? \mapsto PROTECTED \} ) )
\end{schema}


\begin{schema}{AccessNode}
 \Xi NODE \\
 \Xi DOMAIN \\
 user? : USER \\
 userCountry? : COUNTRY \\
 nodeId? : NODEID \\
 accessNodeMetadata? : METADATA \\
 contentOutput! : \power CONTENT 
\where
 nodeId? = nodeId \land accessNodeMetadata? \in roles \limg ( userAccessRigths \limg \{ user? \} \rimg ) \rimg \land ( ( nodeDataCategories \limg \{ accessNodeMetadata? \} \rimg \subseteq CIDCATEGORIES \land userCountry? \neq SWITZERLAND \land contentOutput! = \{ XXXXX \} ) \lor ( ( nodeDataCategories \limg \{ accessNodeMetadata? \} \rimg \cap CIDCATEGORIES =~\emptyset \lor userCountry? = SWITZERLAND ) \land contentOutput! = nodeDataContents \limg \{ accessNodeMetadata? \} \rimg ) )
\end{schema}


\begin{schema}{AccessBulk}
 \Xi DOMAIN \\
 \Xi NODE \\
 \Delta CIDBULKLOG \\
 user? : USER \\
 nodeId? : NODEID \\
 userCountry? : COUNTRY \\
 contentOutput! : \power CONTENT 
\where
 ( ROLEBULKCID \in userAccessRigths \limg \{ user? \} \rimg \land userCountry? = SWITZERLAND \land \ran nodeDataCategories \cap CIDCATEGORIES \neq \emptyset \land cidBulkAccess' = cidBulkAccess \cap \{ ( user? , nodeId? ) \} \land contentOutput! = \ran nodeDataContents \land nodeId? = nodeId ) \lor ( ( ROLEBULK \in userAccessRigths \limg \{ user? \} \rimg \lor ROLEBULKCID \in userAccessRigths \limg \{ user? \} \rimg ) \land cidBulkAccess' = cidBulkAccess \land \ran nodeDataCategories \cap CIDCATEGORIES =~\emptyset \land contentOutput! = \ran nodeDataContents \land nodeId? = nodeId )
\end{schema}


\begin{schema}{AssignDataOwner}
 \Delta DOMAIN \\
 metadata? : METADATA \\
 dataOwnerInput? : ENTITY 
\where
 dataOwner' = dataOwner \oplus \{ metadata? \mapsto dataOwnerInput? \} \\
 roles' = roles \\
 userAccessRigths' = userAccessRigths
\end{schema}


\begin{schema}{ClassifyDataCategory}
 \Delta DOMAIN \\
 metadata? : METADATA \\
 dataCategory? : DATACATEGORY 
\where
 dataClassification' = dataClassification \oplus \{ metadata? \mapsto dataCategory? \} \\
 roles' = roles \\
 userAccessRigths' = userAccessRigths
\end{schema}


\begin{zed}ImplementDataClassification \defs AssignDataOwner \land ClassifyDataCategory
\end{zed}


\begin{schema}{RecycleData}
 \Delta DOMAIN \\
 metadata? : METADATA 
\where
 metadata? \in dataOwnerMetadata \\
 metadata? \in classificationMetadata \\
 dataClassification' = \{ metadata? \} \ndres dataClassification \\
 dataOwner' = \{ metadata? \} \ndres dataOwner \\
 roles' = roles \\
 teams' = teams \\
 userAccessRigths' = userAccessRigths
\end{schema}


\begin{schema}{BulkCIDAccessUsersList}
 \Xi DOMAIN \\
 \Xi NODE \\
 BulkCIDAccessUsersList! : \power USER 
\where
 BulkCIDAccessUsersList! = \dom ( userAccessRigths \rres \{ ROLEBULKCID \} )
\end{schema}