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!
|
| _version_ | 1841530406567936000 |
|---|---|
| author | Cong-hua ZHOU Wei-he CHEN Zhi-feng LIU |
| author_facet | Cong-hua ZHOU Wei-he CHEN Zhi-feng LIU |
| author_sort | Cong-hua ZHOU |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-d2bb257ebd0e413ab5ddfb2998273ff3 |
| institution | Kabale University |
| issn | 2096-109X |
| language | English |
| publishDate | 2016-03-01 |
| publisher | POSTS&TELECOM PRESS Co., LTD |
| record_format | Article |
| series | 网络与信息安全学报 |
| spelling | doaj-art-d2bb257ebd0e413ab5ddfb2998273ff32025-01-15T03:04:26ZengPOSTS&TELECOM PRESS Co., LTD网络与信息安全学报2096-109X2016-03-012526759544438Formal specification and security verification of usage control model based on PATCong-hua ZHOUWei-he CHENZhi-feng LIUUsage 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.http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2909-109x.2016.00038UCONformal specificationsecurity analysismodel checking |
| spellingShingle | Cong-hua ZHOU Wei-he CHEN Zhi-feng LIU Formal specification and security verification of usage control model based on PAT 网络与信息安全学报 UCON formal specification security analysis model checking |
| title | Formal specification and security verification of usage control model based on PAT |
| title_full | Formal specification and security verification of usage control model based on PAT |
| title_fullStr | Formal specification and security verification of usage control model based on PAT |
| title_full_unstemmed | Formal specification and security verification of usage control model based on PAT |
| title_short | Formal specification and security verification of usage control model based on PAT |
| title_sort | formal specification and security verification of usage control model based on pat |
| topic | UCON formal specification security analysis model checking |
| url | http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2909-109x.2016.00038 |
| work_keys_str_mv | AT conghuazhou formalspecificationandsecurityverificationofusagecontrolmodelbasedonpat AT weihechen formalspecificationandsecurityverificationofusagecontrolmodelbasedonpat AT zhifengliu formalspecificationandsecurityverificationofusagecontrolmodelbasedonpat |