[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.
|