{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:12:47Z","timestamp":1763467967336},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642124587"},{"type":"electronic","value":"9783642124594"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12459-4_6","type":"book-chapter","created":{"date-parts":[[2010,4,29]],"date-time":"2010-04-29T06:49:38Z","timestamp":1272523778000},"page":"66-80","source":"Crossref","is-referenced-by-count":26,"title":["Model Checking of Security-Sensitive Business Processes"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Serena Elisa","family":"Ponta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1145\/1133058.1133079","volume-title":"SACMAT","author":"A. Schaad","year":"2006","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, New York (2006)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Cerone, A., Xiangpeng, Z., Krishnan, P.: Modelling and resource allocation planning of BPEL workflows under security constraints. TR 336, UNU-IIST (2006), http:\/\/www.iist.unu.edu\/","DOI":"10.1007\/11841760_36"},{"key":"6_CR3","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 2007, pp. 201\u2013210 (2007)","DOI":"10.1109\/SECUREWARE.2007.4385334"},{"key":"6_CR4","volume-title":"Petri Net Theory and the Modeling of Systems","author":"J.L. Peterson","year":"1981","unstructured":"Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall, Englewood Cliffs (1981)"},{"key":"6_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"730","DOI":"10.1007\/978-3-540-30227-8_68","volume-title":"Logics in Artificial Intelligence","author":"A. Armando","year":"2004","unstructured":"Armando, A., Compagna, L.: SATMC: a SAT-based model checker for security protocols. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 730\u2013733. Springer, Heidelberg (2004)"},{"key":"6_CR6","volume-title":"IJIS","author":"A. Armando","year":"2007","unstructured":"Armando, A., Compagna, L.: Sat-based model-checking for security protocols analysis. In: IJIS. Springer, Heidelberg (2007)"},{"key":"6_CR7","unstructured":"OASIS: Web Services Business Process Execution Language Version 2.0 (2007), http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/OS\/wsbpel-v2.0-OS.html"},{"issue":"2","key":"6_CR8","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/2.485845","volume":"29","author":"R.S. Sandhu","year":"1996","unstructured":"Sandhu, R.S., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-based access control models. Computer\u00a029(2), 38\u201347 (1996)","journal-title":"Computer"},{"key":"6_CR9","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/1063979.1063990","volume-title":"SACMAT","author":"V. Atluri","year":"2005","unstructured":"Atluri, V., Warner, J.: Supporting conditional delegation in secure workflow management systems. In: SACMAT, pp. 49\u201358. ACM Press, New York (2005)"},{"key":"6_CR10","first-page":"623","volume-title":"AAAI 1998","author":"E. Giunchiglia","year":"1998","unstructured":"Giunchiglia, E., Lifschitz, V.: An action language based on causal explanation: Preliminary report. In: AAAI 1998, pp. 623\u2013630. AAAI Press, Menlo Park (1998)"},{"key":"6_CR11","unstructured":"Ferraris, P., Giunchiglia, E.: Planning as satisfiability in nondeterministic domains. In: AAAI 2000 and IAAI 2000, pp. 748\u2013753. AAAI Press \/ The MIT Press (2000)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Armando, A., Ponta, S.E.: Model checking of security-sensitive business processes (2009), http:\/\/www.ai-lab.it\/serena\/tr090724.pdf","DOI":"10.1007\/978-3-642-12459-4_6"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, H.P., He\u00e1m, P.C., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"6_CR14","first-page":"385","volume-title":"CSF-20","author":"A. Armando","year":"2007","unstructured":"Armando, A., Carbone, R., Compagna, L.: LTL model checking for security protocols. In: CSF-20, pp. 385\u2013396. IEEE Computer Society, Los Alamitos (2007)"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1456396.1456397","volume-title":"FMSE","author":"A. Armando","year":"2008","unstructured":"Armando, A., Carbone, R., Compagna, L., Cu\u00e9llar, J., Tobarra, M.L.: Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps. In: FMSE, pp. 1\u201310. ACM, New York (2008)"},{"key":"6_CR16","unstructured":"Kautz, H., McAllester, H., Selman, B.: Encoding Plans in Propositional Logic. In: KR, pp. 374\u2013384 (1996)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00199-4_1","volume-title":"Engineering Secure Software and Systems","author":"C. Wolter","year":"2009","unstructured":"Wolter, C., Miseldine, P., Meinel, C.: Verification of business process entailment constraints using SPIN. In: Massacci, F., Redwine Jr., S.T., Zannone, N. (eds.) ESSoS 2009. LNCS, vol.\u00a05429. Springer, Heidelberg (2009)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/978-3-540-30144-8_19","volume-title":"Information Security","author":"D.P. Guelev","year":"2004","unstructured":"Guelev, D.P., Ryan, M., Schobbens, P.Y.: Model-checking access control policies. In: Zhang, K., Zheng, Y. (eds.) ISC 2004. LNCS, vol.\u00a03225, pp. 219\u2013230. Springer, Heidelberg (2004)"},{"key":"6_CR19","unstructured":"SAP NetWeaver Business Process Management, http:\/\/www.sap.com\/platform\/netweaver\/components\/sapnetweaverbpm\/index.epx"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects in Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12459-4_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:41:48Z","timestamp":1619782908000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12459-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642124587","9783642124594"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12459-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}