Formal specification and security verification of usage control model based on PAT
Usage control (UCON) is an access control model to enforce digital resources protection in highly distributed, heterogeneous network computing environment. Firstly, each core model of UCON was specified formally with TCSP#, and a combination specification mechanism was proposed for general UCON. Sec...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
POSTS&TELECOM PRESS Co., LTD
2016-03-01
|
| Series: | 网络与信息安全学报 |
| Subjects: | |
| Online Access: | http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2909-109x.2016.00038 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | Usage control (UCON) is an access control model to enforce digital resources protection in highly distributed, heterogeneous network computing environment. Firstly, each core model of UCON was specified formally with TCSP#, and a combination specification mechanism was proposed for general UCON. Secondly, as the basis of the security analysis, the concepts and calculation method of the reachable space were given. Various combination mechanisms of processes based on single-session was presented to achieve formal specifications of complex concurrent sessions, timings and nondeterminism. Then the reachable space of combined processes was the desired space. Finally, the security analysis method based on the reachable space and the conflict analysis of access control policies based on the equivalent checking in process algebras were proposed for UCON model. All the proposed work had been formal checked in PAT. The experiment result shows that the proposed approaches are feasible, and PAT is a really great tool for the systematic formal specification and security analysis of UCON. |
|---|---|
| ISSN: | 2096-109X |