{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,10]],"date-time":"2025-12-10T08:31:58Z","timestamp":1765355518769,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642144776"},{"type":"electronic","value":"9783642144783"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14478-3_22","type":"book-chapter","created":{"date-parts":[[2010,7,23]],"date-time":"2010-07-23T16:56:16Z","timestamp":1279904176000},"page":"214-223","source":"Crossref","is-referenced-by-count":11,"title":["Concurrent Usage Control Implementation Verification Using the SPIN Model Checker"],"prefix":"10.1007","author":[{"given":"P. V.","family":"Rajkumar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S. K.","family":"Ghosh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Dasgupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"22_CR1","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1145\/984334.984339","volume":"7","author":"J. Park","year":"2004","unstructured":"Park, J., Sandhu, R.: The UCON ABC usage control model. ACM Transactions on Information and System Security\u00a07(1), 128\u2013174 (2004)","journal-title":"ACM Transactions on Information and System Security"},{"issue":"4","key":"22_CR2","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/1108906.1108908","volume":"8","author":"X. Zhang","year":"2005","unstructured":"Zhang, X., Parisi-Presicce, F., Sandhu, R., Park, J.: Formal model and policy specification of usage control. ACM Transactions on Information and System Security\u00a08(4), 351\u2013387 (2005)","journal-title":"ACM Transactions on Information and System Security"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Zhang, X., Sandhu, R.: Safety analysis of usage control authorization models. In: Proceedings of the 2006 ACM Symposium on Information, Computer and Communications Security, Taipei, Taiwan, pp. 243\u2013254 (2006)","DOI":"10.1145\/1128817.1128853"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Wing, J.M.: A symbiotic relationship between formal methods and security. In: Proceedings of the Computer Security, Dependability and Assurance: From Needs to Solutions, York, UK, pp. 26\u201338 (1998)","DOI":"10.1109\/CSDA.1998.798355"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Naldurg, P., Schwoon, S., Rajamani, S., Lambert, J.: NETRA: Seeing through access control. In: The 4th ACM Workshop on Formal Methods in Security Engineering, Fairfax, Virginia, pp. 55\u201366 (2006)","DOI":"10.1145\/1180337.1180343"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Guelev, D.P., Ryan, M., Schobbens, P.: Model checking access control policies. In: Proceedings of the Seventh Information Security Conference, Palo Alto, USA, pp. 219\u2013230 (2004)","DOI":"10.1007\/978-3-540-30144-8_19"},{"issue":"1","key":"22_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/JCS-2008-16101","volume":"16","author":"N. Zhang","year":"2007","unstructured":"Zhang, N., Guelev, D.P., Ryan, M.: Synthesising verified access control systems through model checking. Journal of Computer Security\u00a016(1), 1\u20136 (2007)","journal-title":"Journal of Computer Security"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Martin, E., Xie, T.: A fault model and mutation testing of access control policies. In: Proceedings of the 16th ACM International Conference on World Wide Web, New York, USA, pp. 667\u2013676 (2007)","DOI":"10.1145\/1242572.1242663"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Pretschner, A., Hilty, M., Basin, D., Schaefer, C., Walter, T.: Mechanisms for usage control. In: ACM Symposium on Information, Computer and Communications Security, Tokyo, Japan, pp. 240\u2013244 (2008)","DOI":"10.1145\/1368310.1368344"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Janicke, H., Cau, A., Siewe, F., Zedan, H.: Concurrent enforcement of usage control policies. In: Proceedings of the IEEE Workshop on Policies for Distributed Systems and Networks, Palisades, NY, USA, pp. 111\u2013118 (June 2008)","DOI":"10.1109\/POLICY.2008.44"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"issue":"6","key":"22_CR12","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in c. IEEE Transactions on Software Engineering\u00a030(6), 388\u2013402 (2004)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. on Software Engineering\u00a023, 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: A new symbolic model verifier. In: Proceedings of the 11th International Conference on Computer Aided Verification,Trento, Italy, pp. 495\u2013499 (1996)","DOI":"10.1007\/3-540-48683-6_44"},{"key":"22_CR15","unstructured":"Lffer, S., Serhrouchni, A.: Creating implementations from promela models. In: Proceedings of Second SPIN Workshop, New Jersey, USA (1996)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Rajkumar, P.V., Ghosh, S.K., Dasgupta, P.: An end to end correctness verification approach for application specific usage control. In: Proceedings of the Fourth IEEE International Conference on Industrial and Information Systems, pp. 122\u2013136 (December 2009)","DOI":"10.1109\/ICIINFS.2009.5429902"},{"issue":"3","key":"22_CR17","first-page":"116","volume":"1","author":"P.V. Rajkumar","year":"2009","unstructured":"Rajkumar, P.V., Ghosh, S.K., Dasgupta, P.: Application specific usage control implementation verification. International Journal of Network Security and Its Applications\u00a01(3), 116\u2013128 (2009)","journal-title":"International Journal of Network Security and Its Applications"}],"container-title":["Communications in Computer and Information Science","Recent Trends in Network Security and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14478-3_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T08:45:44Z","timestamp":1740300344000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14478-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642144776","9783642144783"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14478-3_22","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2010]]}}}