## 4 Proposed Method
### Policy Optimization with Separation-of-Duty Constraints
#### 4.2.2 Construction of t-m MEAR Constraints from k-n SOAR Constraints  
In this subsection, we determine how to construct MEAR constraints for the given SOAR constraints. Using the notions of the \(k\)-\(n\) SOAR constraint and the \(t\)-\(m\) MEAR constraint, as well as the status function \(\mathit{user\_rules_{\gamma}}(u)\) in Definition 6, we can define the safety and satisfiability of the system status as the following. **Definition 6**: _(Safety of the system status, \(\mathit{safe}_{\text{sant}}(\gamma)\)) Given an ABAC system status \(\gamma\) and a \(k\)-\(n\) SOAR constraint \(\mathit{soar}=\)\(<\)\(\mathit{lar}_{1}\), \(\mathit{ar}_{2}\),... \(\mathit{ar}_{n}\)\(\mathit{l}\)\(\mathit{k}\)\(\mathit{\succ}\), if any set of (\(k-\)\(-\)\(1\)) users cannot have all the \(n\) rules under \(\gamma\), then \(\gamma\) is safe with respect to soar, which is denoted as \(\mathit{safe}_{\text{sant}}(\gamma)=1\). Otherwise, \(\gamma\) is unsafe with respect to soar, which is denoted as \(\mathit{safe}_{\text{sant}}(\gamma)=0\). Let the set of different \(k\)-\(n\) SOAR constraints be \(\xi=\)\(\{\mathit{soar}_{1}\), \(\mathit{soar}_{2}\),... \(\mathit{l}\); if \(\gamma\) is safe with respect to each \(\mathit{soar}_{i}\), then \(\gamma\) is safe with respect to \(\xi\), which is denoted as \(\mathit{safe}_{\xi}(\gamma)=1\). Otherwise, \(\gamma\) is unsafe with respect to \(\xi\), which is denoted as \(\mathit{safe}_{\xi}(\gamma)=0\)._  
The safety of the system status is formally expressed as:  
\[\forall\{u_{1},u_{2},\ldots,u_{k-1}\}\subset U:\{\mathit{ar}_{1},\mathit{ar} _{2},\ldots,\mathit{ar}_{n}\}_{i=1}^{k-1}\mathit{user\_rules_{\gamma}}(u_{i}) \Rightarrow\mathit{safe}_{\text{sant}}(\gamma)\;=1. \tag{10}\]  
The unsafety of the system status is formally expressed as:  
\[\exists|u_{1},u_{2},\ldots,u_{k-1}|\subset U:\mathop{\cup}\limits_{i=1}^{k-1 }\mathit{user\_rules_{\gamma}}(u_{i})\supseteq\{\mathit{ar}_{1},\mathit{ar}_{ 2},\ldots,\mathit{ar}_{n}\}\Rightarrow\mathit{safe}_{\text{sant}}(\gamma)\;=0. \tag{11}\]  
**Definition 7**: _(Satisfiability of the system status, \(\mathit{satisfied}_{\text{max}}(\gamma)\)) Given an ABAC system status \(\gamma\) and a \(t\)-\(m\) MEAR constraint \(\mathit{near}=\)\(<\)\(\mathit{lar}_{1}\), \(\mathit{ar}_{2}\),... \(\mathit{ar}_{n}\)\(\mathit{l}\)\(\mathit{\succ}\), if no user is allowed to have \(t\) or more of these \(m\) rules under \(\gamma\), then \(\gamma\) is satisfied with respect to \(\mathit{near}\), which is denoted as \(\mathit{satisfied}_{\text{max}}(\gamma)=1\). Otherwise, \(\gamma\) is unsatisfied with respect to \(\mathit{near}\), which is denoted as \(\mathit{satisfied}_{\text{max}}(\gamma)=0\). Let the set of different \(t\)-\(m\) MEAR constraints be \(\psi\) = \(\{\mathit{near}_{1}\), \(\mathit{near}_{2}\),... \(\mathit{l}\); if \(\gamma\) is satisfied with respect to each \(\mathit{near}_{i}\), then \(\gamma\) is satisfied with respect to \(\psi\), which is denoted as \(\mathit{satisfied}_{\psi}(\gamma)=0\)._  
The satisfiability of the system status is formally expressed as:  
\[\forall u\in U:\lvert\mathit{user\_rules_{\gamma}}(u)\cap\{\mathit{ar}_{1}, \mathit{ar}_{2},\ldots\mathit{ar}_{n}\}\rvert<\mathit{t}\Rightarrow\mathit{ satis}\,\mathit{fied}_{\text{max}}(\gamma)=1. \tag{12}\]  
The unsatisfiability of the system status is formally expressed as:  
\[\exists u\in U:\lvert\mathit{user\_rules_{\gamma}}(u)\cap\{\mathit{ar}_{1}, \mathit{ar}_{2},\ldots\mathit{ar}_{n}\}\rvert\geq\mathit{t}\Rightarrow\mathit{ satis}\,\mathit{fied}_{\text{max}}(\gamma)=0. \tag{13}\]  
**Statement 1**: _Given an ABAC system status \(\gamma\) and a set of SOAR constraints \(\xi=\)\(\{\mathit{soar}_{1}\), \(\mathit{soar}_{2}\),... \(\mathit{l}\), the process for verifying whether \(\gamma\) is safe with respect to \(\xi\) is in \(P\)._  
**Proof. ** We prove this statement through the following three steps: (1) Use status function \(\mathit{user\_rules_{\gamma}}(\mathit{l})\) and identify \(\mathit{user\_rules_{\gamma}}(u)\) for some user \(u\) under \(\gamma\) (2).