{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:40:34Z","timestamp":1725493234335},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540766483"},{"type":"electronic","value":"9783540766506"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-76650-6_4","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T07:12:49Z","timestamp":1193382769000},"page":"37-56","source":"Crossref","is-referenced-by-count":11,"title":["Formal Engineering of XACML Access Control Policies in VDM++"],"prefix":"10.1007","author":[{"given":"Jeremy W.","family":"Bryans","sequence":"first","affiliation":[]},{"given":"John S.","family":"Fitzgerald","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Andrews, D.J. (ed.): Information technology \u2013 Programming languages, their environments and system software interfaces \u2013 Vienna Development Method \u2013 Specification Language \u2013 Part 1: Base language. International Organization for Standardization, International Standard ISO\/IEC 13817-1 (December 1996)"},{"key":"4_CR2","unstructured":"Becker, M.Y., Fournet, C., Gordon, A.D.: SecPAL: Design and semantics of a decentralized authorisation language. Technical Report MSR-TR-2006-120, Microsoft Research (September 2006)"},{"key":"4_CR3","volume-title":"2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)","author":"J.W. Bryans","year":"2006","unstructured":"Bryans, J.W., Fitzgerald, J.S., Jones, C.B., Mozolevsky, I.: Formal modelling of dynamic coalitions, with an application in chemical engineering. In: 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), IEEE Computer Society Press, Los Alamitos (2006) Also available as Technical Report CS-TR-981, Newcastle University, UK (to appear)"},{"key":"4_CR4","unstructured":"Bryans, J.W., Fitzgerald, J.S., Periorellis, P.: Model based analysis and validation of access control policies. Technical Report CS-TR-976, Newcastle University, School of Computing Science (July 2006)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-540-39650-5_2","volume-title":"ESORICS 2003","author":"D. Domingos","year":"2003","unstructured":"Domingos, D., Rito-Silva, A., Veiga, P.: Authorization and access control in adaptive workflows. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol.\u00a02808, pp. 23\u201338. Springer, Heidelberg (2003)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Specifying and reasoning about dynamic access-control policies. In: Proceedings of the International Joint Conference on Automated Reasoning (August 2006)","DOI":"10.1007\/11814771_51"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/1062455.1062502","volume-title":"ICSE 2005","author":"K. Fisler","year":"2005","unstructured":"Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and change-impact analysis of access-control policies. In: ICSE 2005, pp. 196\u2013205. ACM Press, New York (2005)"},{"key":"4_CR8","volume-title":"Modelling Systems: Practical Tools and Techniques in Software Development","author":"J.S. Fitzgerald","year":"1998","unstructured":"Fitzgerald, J.S., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development. Cambridge University Press, Cambridge (1998)"},{"key":"4_CR9","volume-title":"2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)","author":"J.S. Fitzgerald","year":"2006","unstructured":"Fitzgerald, J.S., Larsen, P.G.: Triumphs and challenges for the industrial application of model-oriented formal methods. In: 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), IEEE Computer Society Press, Los Alamitos (2006) Also available as Technical Report CS-TR-999, Newcastle University, UK (to appear)"},{"key":"4_CR10","volume-title":"Validated Designs for Object-oriented Systems","author":"J.S. Fitzgerald","year":"2004","unstructured":"Fitzgerald, J.S., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-oriented Systems. Springer, Heidelberg (2004)"},{"key":"4_CR11","unstructured":"Hughes, G., Bultan, T.: Automated verification of access control policies. Technical Report 2004-22, University of California, Santa Barbara (2004)"},{"key":"4_CR12","unstructured":"Humenn, P.: The formal semantics of XACML, available at http:\/\/lists.oasis-open.org\/archives\/xacml\/200310\/pdf00000.pdf"},{"key":"4_CR13","series-title":"International Series in Computer Science","volume-title":"Systematic Software Development using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development using VDM. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1990)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/978-3-540-75221-9_16","volume-title":"Essays in Honour of Dines Bj\u00f8rner and Zhou Chaochen on the Occasion of their 70th Birthdays","author":"C.B. Jones","year":"2007","unstructured":"Jones, C.B., Hayes, I.J., Jackson, M.A.: Deriving specifications for systems that are connected to the physical world. In: Woodcock, J. (ed.) Essays in Honour of Dines Bj\u00f8rner and Zhou Chaochen on the Occasion of their 70th Birthdays. LNCS, vol.\u00a04700, pp. 364\u2013390. Springer, Heidelberg (2007)"},{"key":"4_CR15","unstructured":"M\u00e9ry, D., Merz, S.: Event systems and access control. In: Gollmann, D., J\u00fcrjens, J. (eds.) 6th International Workshop on Issues in the Theory of Security, Vienna, Austria, IFIP WG 1.7, Vienna University of Technology, pp. 40\u201354 (2006)"},{"key":"4_CR16","unstructured":"OASIS: eXtensible Access Control Markup Language (XACML) version 2.0. Technical report, OASIS (February 2005)"},{"key":"4_CR17","unstructured":"Overture Group: The VDM Portal (2007), http:\/\/www.vdmportal.org"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Zhang, N., Ryan, M.D., Guelev, D.: Synthesising verified access control systems through model checking. Journal of Computer Security (in print, 2007)","DOI":"10.3233\/JCS-2008-16101"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-76650-6_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:57:17Z","timestamp":1619521037000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-76650-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540766483","9783540766506"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-76650-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}