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

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

网络与信息安全学报 ›› 2016, Vol. 2 ›› Issue (3): 52-67.doi: 10.11959/j.issn.2909-109x.2016.00038

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

周从华(),陈伟鹤,刘志锋

江苏大学计算机科学与通信工程学院，江苏镇江 212013

修回日期:2016-03-05 出版日期:2016-12-01 发布日期:2016-04-20
作者简介:周从华（1978-），男，江苏盐城人，博士，江苏大学副教授，主要研究方向为访问控制、形式化方法。|陈伟鹤（1974-），男，江苏丹阳人，博士，江苏大学副教授，主要研究方向为访问控制、数据挖掘。|刘志锋（1981-），男，江苏无锡人，博士，江苏大学副教授，主要研究方向为访问控制、形式化方法。
基金资助:
国家自然科学基金资助项目(61300228)

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

Cong-hua ZHOU(),Wei-he CHEN,Zhi-feng LIU

School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013, China

Revised:2016-03-05 Online:2016-12-01 Published:2016-04-20
Supported by:
The National Natural Science Foundation of China(61300228)

摘要/Abstract

摘要：

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

关键词: 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.

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

中图分类号:

TP309.7

周从华,陈伟鹤,刘志锋. 基于PAT的使用控制模型的形式化规约与安全性分析[J]. 网络与信息安全学报, 2016, 2(3): 52-67.

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.

图/表 1

参考文献 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.

规模	性能参数	简单安全性	简单可用性	限界安全性	活性	包含性	完全性	相容性	公平性
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

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

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

在线阅读

pdf下载

可视化

被引次数

摘要/Abstract

引用本文

使用本文

图/表 1

参考文献 22

相关文章 3

Metrics

推荐阅读 0

[1]	张启智, 赵毅强, 高雅, 马浩诚. 基于模型检测的硬件木马检测技术研究[J]. 网络与信息安全学报, 2021, 7(2): 57-63.
[2]	孟博,刘加兵,刘琴,王潇潇,郑旭睿,王德军. 智能合约安全综述[J]. 网络与信息安全学报, 2020, 6(3): 1-13.
[3]	王众,韩益亮. 密文长度可变的Simple Matrix加密方案[J]. 网络与信息安全学报, 2018, 4(4): 56-62.