基于PAT的使用控制模型的形式化规约与安全性分析

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

Abstract

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.

Key words: UCON, formal specification, security analysis, model checking

CLC Number:

TP309.7

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.

Figures/Tables 1

References 22

[1]	PFLEEGER C P , PFLEEGER S L . Security in computing[M]. Prentice Hall Professional Technical Reference, 2002.
[2]	SANDHU R S , COYNE E J . FEINSTEIN H L , et al. Role-based access control models[J]. Computer, 1996,29(2): 38-47.
[3]	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.
[4]	PARK J , SANDHU R . The UCON ABC usage control model[J]. ACM Transactions on Information and System Security(TISSEC), 2004,7(1): 128-174.
[5]	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.
[6]	ZHANG X . Formal model and analysis of usage control[D]. Fairfax County, Virgina: George Mason University, 2006.
[7]	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.
[8]	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.
[9]	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.
[10]	LAZOUSKI A , MARTINELLI F , MORI P , . Usage control in computer security: a survey[J]. Computer Science Review, 2010,4(2): 81-99.
[11]	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.
[1]	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.
[13]	HOLZMANN G J . The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997,23(5): 279-295.
[1]	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.
[15]	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.
[16]	VARDI M Y . An automata-theoretic approach to linear temporal logic[M]// Logics for concurrency. Berlin Heidelberg: Springer, 1996.238-266.
[17]	MCLEAN J . A comment on the ‘basic security theorem’of bell and LaPadula[J]. Information Processing Letters, 1985,20(2): 67-70.
[18]	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.
[19]	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.
[20]	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.
[21]	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.
[22]	LAMPORT L . The temporal logic of actions[J]. ACM Transactions on Programming Languages and Systems (TOPLAS), 1994,16(3): 872-923.

Metrics

Recommended 0

No Suggested Reading articles found!

规模	性能参数	简单安全性	简单可用性	限界安全性	活性	包含性	完全性	相容性	公平性
2,3	Visited States	51	7	7	61	11	667	2	1 855
	Total Transitions	80	70	70	630	112	8243	1	16 711
	Time/s	0.126 849 7	0.080 961 3	0.009 358	0.050 039 1	0.009 759 5	0.276 498	0.005 870 8	0.442 401 9
	Memory/KB	9 320.76	9 112.904	9 135.736	12 821.24	9 496.912	21 611.824	32 660.28	14 762.848
4,4	Visited States	232	473	473	12 297	711	90 130	2	189 955
	Total Transitions	523	10 961	10 961	285 347	16 345	176 152	1	1 079 567
	Time/s	0.088 303 4	0.499 98	0.493 146 2	12.169 622 8	0.624 068 8	3.289 180 3	0.004 463 5	32.791 591 8
	Memory/KB	9 330.84	25 630.4	27 264.616	444 924.864	37 957.12	103 927.336	32 653.784	266 899.36
8,6	Visited States	838	235	235	N/A	3 412	2 027 340	2	N/A
	Total Transitions	2 461	328	328	N/A	5 084	4 019 980	1	N/A
	Time/s	0.139 493 4	0.083 753 6	0.031 495 6	N/A	0.269 614 8	104.038 858 3	0.052 275 4	N/A
	Memory/KB	11 348.336	12 065.008	12 517.896	N/A	20 573.32	2 178 426.368	32 793.048	N/A

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

RichHTML

PDF下载

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 1

References 22

Related Articles 4

Metrics

Recommended 0

[1]	Qizhi ZHANG, Yiqiang ZHAO, Ya GAO, Haocheng MA. Survey on model checking based hardware Trojan detection technology [J]. Chinese Journal of Network and Information Security, 2021, 7(2): 57-63.
[2]	Bo MENG,Jiabing LIU,Qin LIU,Xiaoxiao WANG,Xurui ZHENG,Dejun WANG. Survey of smart contract security [J]. Chinese Journal of Network and Information Security, 2020, 6(3): 1-13.
[3]	Zhong WANG,Yiliang HAN. Simple Matrix encryption scheme with variable ciphertext length [J]. Chinese Journal of Network and Information Security, 2018, 4(4): 56-62.
[4]	Shun HU,Jian WENG,Jia-nan LIU. An ownership transfer protocol for wearable devices [J]. Chinese Journal of Network and Information Security, 2015, 1(1): 72-80.