# Role-Based Access Control Model for Inter-System Cross-Domain in Multi-Domain Environment
## 6 Model Evaluation
### Security Analysis
#### 6.2.1 Model Confidentiality Analysis
should be established;  
However, due to \(sr\in user\_authorization(u)\) and \(sr\
otin user\_authorization(u)\), conflicts exist;  
Therefore, Formula (29) does not hold; that is, Formulae (27) and (28) cannot hold at the same time;  
It can be proved that RBAC-IC does not meet Formula (27). \(\square\)  
2. Access with specific role without permission;  
\[p\
otin sr\_assignment(sr)\wedge sr\in user\_authorization(u)\wedge s\in user\_session(u)\wedge p\in session\_permission(s) \tag{30}\]  
This formula describes that if user \(u\) authorizes the specific role \(sr\), \(sr\) does not assign permission \(p\), but the user still activates session \(s\), and \(p\) is used in session \(s\). This indicates that the user has used an unassigned permission for unauthorized access. The proof process for RBAC-IC not meeting Formula (30) is similar to Formula (27). 3. Access with expired specific role;  
\[current\_time\
otin sr[valid\_time]\wedge s\in user\_session(u)\wedge sr\in session\_sr(s) \tag{31}\]  
This formula describes that the specific role \(sr\) has expired, but user \(u\) can still use \(sr\) in the activated session \(s\). This indicates that the user is using an expired specific role. **Proof that RBAC-IC does not meet Formula (31). **  
Assume that the current time is within the effective time range of the specific role \(sr\); that is, \(sr[valid\_time][min\_time]\leq current\_time\leq sr[valid\_time][max\_time]\);  
If the current time is not within the valid time range; that is, \(sr[valid\_time][min\_time]>current\_time>sr[valid\_time][max\_time]\);  
If there is a case where \(s\) can be activated by the user and \(sr\) can be used in \(s\), Formula (31) holds;  
At the same time. Illustrate the following formula,  
\[current\_time\
otin sr[valid\_time]\wedge current\_time\in sr[valid\_time] \wedge s\in user\_session(u)\wedge sr\in session\_sr(s) \tag{32}\]  
should be established;  
However, \(current\_time\
otin sr[valid\_time]\) and \(current\_time\in sr[valid\_time]\) conflicts exist, and RBAC-IC stipulates that specific roles can only be used within the validity period. Therefore, Formulae (31) and (32) cannot hold at the same time. It can be proved that RBAC-IC does not meet Formula (31). \(\square\)  
6.2.2. Model Constraint Security Analysis  
1. Static mutex constraint; \[static\_mutex(sr_{1},sr_{2})\wedge sr_{1},sr_{2}\in user\_authorization(u)\] (33)  
where \(static\_mutex(sr_{1},sr_{2})\) indicates that specific roles \(sr_{1}\) and \(sr_{2}\) have static mutual exclusion constraints; that is, the two roles cannot be authorized to one user. This formula describes the \(sr_{1}\) and \(sr_{2}\) that authorize the user \(u\) with static mutex constraints at the same time. This indicates that the static mutual exclusion constraint rule of the specific role is violated. **Proof that RBAC-IC does not meet Formula (33). **  
Assume there is user \(u\), and specific roles \(sr_{1}\) and \(sr_{2}\), \(sr_{1}\
eq sr_{2}\), and there is a static mutual exclusion relationship between \(sr_{1}\) and \(sr_{2}\);  
Assume that \(sr_{1}\) is authorized to \(u\), and \(sr_{2}\) is not authorized to \(u\); that is,  
\[static\_mutex(sr_{1},sr_{2})\wedge sr_{1}\in user\_authorization(u)\wedge sr_{2} \
otin user\_authorization(u) \tag{34}\]  
is established;If both \(sr_{1}\) and \(sr_{2}\) are authorized to \(u\), Formula (31) is established; According to the static mutual exclusion relationship between \(sr_{1}\) and \(sr_{2}\), users can only be authorized to a specific role in the specific role set with static mutual exclusion relationship; Therefore, both \(sr_{1}\) and \(sr_{2}\) cannot be authorized to \(u\); It can be proved that RBAC-IC does not meet Formula (33). \(\square\)  
Figure 10 shows an example of a static mutex constraint. 2.