Formal specification and security verification of usage control model based on PAT

Cong-hua ZHOU; Wei-he CHEN; Zhi-feng LIU

doi:10.11959/j.issn.2909-109x.2016.00038

您当前的位置：

首页 >

文章列表页 >

Formal specification and security verification of usage control model based on PAT

academic paper | 更新时间：2024-06-03

- Formal specification and security verification of usage control model based on PAT
- Chinese Journal of Network and Information Security Vol. 2, Issue 3, Pages: 52-67(2016)
- 作者机构：
- 作者简介：
- 基金信息：
- DOI：10.11959/j.issn.2909-109x.2016.00038
  CLC： TP309.7
- Online First：2016-12，
  
  Published：15 March 2016
- 稿件说明：
移动端阅览
Cong-hua ZHOU, Wei-he CHEN, Zhi-feng LIU. Formal specification and security verification of usage control model based on PAT[J]. Chinese Journal of Network and Information Security, 2016, 2(3): 52-67.
DOI：

Cong-hua ZHOU, Wei-he CHEN, Zhi-feng LIU. Formal specification and security verification of usage control model based on PAT[J]. Chinese Journal of Network and Information Security, 2016, 2(3): 52-67. DOI： 10.11959/j.issn.2909-109x.2016.00038.

摘要

使用控制模型UCON是高度分布式、网络化的异构开放式计算环境下实现数字资源保护的新型访问控制模型。首先，利用态式时间进程代数 TCSP#建立了每个 UCON 核模型的形式化规约，以及针对一般化UCON的组合规约机制。其次，提出了各种基于单会话的进程组合机制，实现了复杂并发会话、时间控制与非确定性的形式化规范，从而使组合进程的可达空间即为所求空间。最后，提出了基于可达空间的UCON安全性分析方法，以及基于进程代数等价的控制规则冲突性分析方法。所有的工作都已在PAT上实现，表明所提方法是切实可行的，同时也为UCON的形式化规范与安全性验证寻找到了一个合适的工具。

Abstract

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.

关键词

Keywords

references

PFLEEGER C P , PFLEEGER S L . Security in computing [M ] . Prentice Hall Professional Technical Reference , 2002 .

SANDHU R S , COYNE E J . FEINSTEIN H L , et al . Role-based access control models [J ] . Computer , 1996 , 29 ( 2 ): 38 - 47 .

FERRAIOLO D F , SANDHU R . GAVRILA S , et al . Proposed NIST standard for role-based access control [J ] . ACM Transactions on Information and System Security(TISSEC) , 2001 , 4 ( 3 ): 224 - 274 .

PARK J , SANDHU R . The UCON ABC usage control model [J ] . ACM Transactions on Information and System Security(TISSEC) , 2004 , 7 ( 1 ): 128 - 174 .

ZHANG X , PARISI-PRESICCE F , SANDHU R , et al . Formal model and policy specification of usage control [J ] . ACM Transactions on Information and System Security (TISSEC) , 2005 , 8 ( 4 ): 351 - 387 .

ZHANG X . Formal model and analysis of usage control [D ] . Fairfax County , Virgina: George Mason University , 2006 .

JANICKE H , CAU A , ZEDAN H . A note on the formalisation of UCON [C ] // The 12th ACM Symposium on Access Control Models and Technologies .c 2007 : 163 - 168 .

MARTINELLI F , CAU A , ZEDAN H . A model for usage control in GRID systems [C ] // The Third International Conference on Security and Privacy in Communications Networks and the Workshops .c 2007 : 520 - 520 .

JAGADEESAN R , MARRERO W , PITCHER C et al . Timed constraint programming: a declarative approach to usage control [C ] // The 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming .c 2005 : 164 - 175 .

LAZOUSKI A , MARTINELLI F , MORI P , . Usage control in computer security: a survey [J ] . Computer Science Review , 2010 , 4 ( 2 ): 81 - 99 .

ZHANG X , SANDHU R , PARISI-PRESICCE F . Safety analysis of usage control authorization models [C ] // The 2006 ACM Symposium on Information, Computer and Communications Security .c 2006 , 6 243 - 254 .

RAJKUMAR P V , GHOSH S K , DASGUPTA P . Concurrent usage control implementation verification using the SPIN model checker [C ] // The Third International, CNSA 2010, Chennai, India . Berlin Heidelberg Springer .c 2010 ： 214 - 223 .

HOLZMANN G J . The model checker SPIN [J ] . IEEE Transactions on Software Engineering , 1997 , 23 ( 5 ): 279 - 295 .

SUN J , LIU Y , DONG J S et al . PAT: towards flexible verification under fairness [C ] // The 21st International Conference on Computer Aided Verification .c 2009 ： 709 - 714 .

SUN J , LIU Y , DONG J S et al . Modeling and verifying hierarchical real-time systems using stateful timed csp [J ] . ACM Transactions on Software Engineering and Methodology(TOSEM) , 2013 , 22 ( 1 ): 139 - 176 .

VARDI M Y . An automata-theoretic approach to linear temporal logic [M ] // Logics for concurrency . Berlin Heidelberg: Springer , 1996 . 238 - 266 .

MCLEAN J . A comment on the ‘basic security theorem’of bell and LaPadula [J ] . Information Processing Letters , 1985 , 20 ( 2 ): 67 - 70 .

KATT B , HAFNER M , ZHANG X . A usage control policy specification with petri nets [C ] // The 5th International Conference on Collaborative Computing: Networking, Applications and Worksharing .c 2009 ： 1 - 8 .

LI N , TRIPUNITARA M V . Security analysis in role-based access control [J ] . ACM Transactions on Information and System Security (TISSEC) , 2006 , 9 ( 4 ): 391 - 420 .

ADI K , BOUZIDA Y , HATTAK I et al . Typing for conflict detection in access control policies [M ] // E-technologies: Innovation in An Open World . Berlin Heidelberg: Springer , 2009 ： 212 - 226 .

ZHANG N , RYAN M , GUELEV D P . Synthesising verified access control systems through model checking [J ] . Journal of Computer Security , 2008 , 16 ( 1 ): 1 - 61 .

LAMPORT L . The temporal logic of actions [J ] . ACM Transactions on Programming Languages and Systems (TOPLAS) , 1994 , 16 ( 3 ): 872 - 923 .

Views

1427

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

5G-based smart airport network security scheme design and security analysis

Survey on model checking based hardware Trojan detection technology

Survey of smart contract security

Simple Matrix encryption scheme with variable ciphertext length

Related Author

Xinxin XING

Qingya ZUO

Jianwei LIU

Qizhi ZHANG

Yiqiang ZHAO

Ya GAO

Haocheng MA

Bo MENG

Related Institution

School of Cyber Science and Technology, Beihang University

International School, Beijing University of Posts and Telecommunications

⁰