{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T20:04:41Z","timestamp":1771704281885,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642299629","type":"print"},{"value":"9783642299636","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29963-6_12","type":"book-chapter","created":{"date-parts":[[2012,4,28]],"date-time":"2012-04-28T12:06:00Z","timestamp":1335614760000},"page":"157-174","source":"Crossref","is-referenced-by-count":4,"title":["Automated Analysis of Infinite State Workflows with Access Control Policies"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/978-3-540-71209-1_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Ben Henda, N., Rezine, A.: Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 721\u2013736. Springer, Heidelberg (2007)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-22438-6_4","volume-title":"Automated Deduction \u2013 CADE-23","author":"F. Alberti","year":"2011","unstructured":"Alberti, F., Armando, A., Ranise, S.: ASASP: Automated Symbolic Analysis of Security Policies. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 26\u201333. Springer, Heidelberg (2011)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Alberti, F., Armando, A., Ranise, S.: Efficient Symbolic Automated Analysis of Administrative Role Based Access Control Policies. In: 6th ACM Symp. on Information, Computer, and Communications Security, ASIACCS (2011)","DOI":"10.1145\/1966913.1966935"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-12459-4_6","volume-title":"Formal Aspects in Security and Trust","author":"A. Armando","year":"2010","unstructured":"Armando, A., Ponta, S.E.: Model Checking of Security-sensitive Business Processes. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol.\u00a05983, pp. 66\u201380. Springer, Heidelberg (2010)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-22444-7_2","volume-title":"Security and Trust Management","author":"A. Armando","year":"2011","unstructured":"Armando, A., Ranise, S.: Automated Symbolic Analysis of ARBAC Policies. In: Cuellar, J., Lopez, J., Barthe, G., Pretschner, A. (eds.) STM 2010. LNCS, vol.\u00a06710, pp. 17\u201334. Springer, Heidelberg (2011)"},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1145\/300830.300837","volume":"2","author":"E. Bertino","year":"1999","unstructured":"Bertino, E., Ferrari, E., Atluri, V.: The specification and enforcement of authorization constraints in workflow management systems. ACM Trans. Inf. Syst. Secur.\u00a02, 65\u2013104 (1999)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Cerone, A., Xiangpeng, Z., Krishnan, P.: Modelling and resource allocation planning of BPEL workflows under security constraints. Technical Report 336, UNU-IIST (2006)","DOI":"10.1007\/11841760_36"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. Technical Report LSV-98-1, LSV ENS Cachan (1998)","DOI":"10.1007\/BFb0028751"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Crampton, J.: A reference monitor for workflow systems with constrained task execution. In: 10th ACM SACMAT, pp. 38\u201347. ACM (2005)","DOI":"10.1145\/1063979.1063986"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Dury, A., Boroday, S., Petrenko, A., Lotz, V.: Formal verification of business workflows and role based access control systems. In: SECURWARE, pp. 201\u20132010 (2007)","DOI":"10.1109\/SECUREWARE.2007.4385334"},{"key":"12_CR11","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (1972)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-36189-8_15","volume-title":"Web Services, E-Business, and the Semantic Web","author":"X. Fu","year":"2002","unstructured":"Fu, X., Bultan, T., Su, J.: Formal Verification of E-Services and Workflows. In: Bussler, C.J., McIlraith, S.A., Orlowska, M.E., Pernici, B., Yang, J. (eds.) CAiSE 2002 and WES 2002. LNCS, vol.\u00a02512, pp. 188\u2013202. Springer, Heidelberg (2002)"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by smt solving: Termination and invariant synthesis. In: LMCS, vol.\u00a06(4) (2010)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"issue":"8","key":"12_CR14","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1145\/360303.360333","volume":"19","author":"M.A. Harrison","year":"1976","unstructured":"Harrison, M.A., Ruzzo, W.L., Ullman, J.D.: Protection in operating systems. Communications of the ACM\u00a019(8), 461\u2013471 (1976)","journal-title":"Communications of the ACM"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Warner, J., Atluri, V.: Inter-Instance Authorization Constraints for Secure Workflow Managment. In: SACMAT, pp. 190\u2013199. ACM (2006)","DOI":"10.1145\/1133058.1133085"},{"issue":"2","key":"12_CR16","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1145\/501963.501966","volume":"4","author":"T. Jaeger","year":"2001","unstructured":"Jaeger, T., Tidswell, J.: Practical safety in flexible access control models. ACM Transaction on Information and System Security\u00a04(2), 158\u2013190 (2001)","journal-title":"ACM Transaction on Information and System Security"},{"issue":"4","key":"12_CR17","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/1187441.1187442","volume":"9","author":"N. Li","year":"2006","unstructured":"Li, N., Tripunitara, M.V.: Security analysis in role-based access control. ACM Transactions on Information and System Security (TISSEC)\u00a09(4), 391\u2013420 (2006)","journal-title":"ACM Transactions on Information and System Security (TISSEC)"},{"key":"12_CR18","unstructured":"Monakova, G., Kopp, O., Leymann, F.: Improving Control Flow Verification in a Business Process using an Extended Petri Net. In: 1st Central-European Workshop on Services and their Composition, ZEUS (2009)"},{"issue":"1","key":"12_CR19","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"s2-30","author":"F.P. Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a Problem of Formal Logic. Proceedings of the London Mathematical Society\u00a0s2-30(1), 264\u2013286 (1930)","journal-title":"Proceedings of the London Mathematical Society"},{"issue":"29","key":"12_CR20","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/2.485845","volume":"2","author":"R. Sandhu","year":"1996","unstructured":"Sandhu, R., Coyne, E., Feinstein, H., Youmann, C.: Role-Based Access Control Models. IEEE Computer\u00a02(29), 38\u201347 (1996)","journal-title":"IEEE Computer"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Schaad, A., Lotz, V., Sohr, K.: A model-checking approach to analysing organisational controls in a loan origination process. In: SACMAT, pp. 139\u2013149. ACM (2006)","DOI":"10.1145\/1133058.1133079"},{"key":"12_CR22","unstructured":"Tripunitara, M.V., Li, N.: The Foundational work of Harrison-Ruzzo-Ullman Revisited. Technical Report CERIAS TR 2006-33, CERIAS and Department of Computer Science. Purdue University (2006)"},{"key":"12_CR23","first-page":"1","volume":"13","author":"Q. Wang","year":"2010","unstructured":"Wang, Q., Li, N.: Satisfiability and resiliency in workflow authorization systems. ACM Trans. Inf. Syst. Secur.\u00a013, 40:1\u201340:35 (2010)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-88313-5_21","volume-title":"Computer Security - ESORICS 2008","author":"Q. Wang","year":"2008","unstructured":"Wang, Q., Li, N., Chen, H.: On the Security of Delegation in Access Control Systems. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol.\u00a05283, pp. 317\u2013332. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Security and Trust Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29963-6_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:23:20Z","timestamp":1620127400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29963-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642299629","9783642299636"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29963-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}