{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T06:41:30Z","timestamp":1648795290128},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,12,30]],"date-time":"2010-12-30T00:00:00Z","timestamp":1293667200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SOCA"],"published-print":{"date-parts":[[2011,6]]},"DOI":"10.1007\/s11761-010-0073-4","type":"journal-article","created":{"date-parts":[[2010,12,29]],"date-time":"2010-12-29T11:04:44Z","timestamp":1293620684000},"page":"105-137","source":"Crossref","is-referenced-by-count":4,"title":["A declarative two-level framework to specify and verify workflow and authorization policies in service-oriented architectures"],"prefix":"10.1007","volume":"5","author":[{"given":"Michele","family":"Barletta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,12,30]]},"reference":[{"key":"73_CR1","doi-asserted-by":"crossref","unstructured":"Armando A, Ponta SE (2009) Model checking of security-sensitive business processes. submitted","DOI":"10.1007\/978-3-642-12459-4_6"},{"issue":"2","key":"73_CR2","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A Armando","year":"2003","unstructured":"Armando A, Ranise S, Rusinowitch M (2003) A rewriting approach to satisfiability procedures. Inf Comput 183(2): 140\u2013164","journal-title":"Inf Comput"},{"key":"73_CR3","unstructured":"AVANTSSAR (2008) Deliverable 5.1: problem cases and their trust and security requirements. Available at http:\/\/www.avantssar.eu"},{"key":"73_CR4","doi-asserted-by":"crossref","unstructured":"Balbiani P, Chevalier Y, El Houri M (2008) A logical approach to dynamic role-based access control. In: Proceedings of AIMSA\u201908, LNCS 5253. Springer","DOI":"10.1007\/978-3-540-85776-1_17"},{"key":"73_CR5","unstructured":"Balbiani P, Chevalier Y, El Houri M (2009) An attribute based framework to express dynamic evolution of services in a distributed environment. submitted"},{"key":"73_CR6","doi-asserted-by":"crossref","unstructured":"Barletta M, Ranise S, Vigan\u00f2 L (2009) Verifying the interplay of authorization policies and workflow in service-oriented architectures. In: Proceedings of the 2009 international symposium on secure computing (SecureCom 2009), vol. 3 of 2009 international conference on computational science and engineering (CSE 2009). IEEE Computer Society Press, pp 289\u2013299. http:\/\/doi.ieeecomputersociety.org\/10.1109\/CSE.2009.172","DOI":"10.1109\/CSE.2009.172"},{"key":"73_CR7","doi-asserted-by":"crossref","unstructured":"Becker MY (2009) Specification and analysis of dynamic authorisation policies. In: Proceedings of the 22nd IEEE computer security foundations symposium (CSF). IEEE Computer Society Press","DOI":"10.1109\/CSF.2009.14"},{"key":"73_CR8","unstructured":"Becker MY, Fournet C, Gordon AD Security policy assertion language (SecPAL). http:\/\/research.microsoft.com\/en-us\/projects\/SecPAL\/"},{"key":"73_CR9","doi-asserted-by":"crossref","unstructured":"Becker MY, Nanz S (2009) A logic for state-modifying authorization policies. ACM transactions on information and system security (TISSEC)","DOI":"10.1145\/1805974.1805976"},{"issue":"6","key":"73_CR10","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1109\/MIS.2006.117","volume":"21","author":"B Beckert","year":"2006","unstructured":"Beckert B, Hoare T, H\u00e4hnle R, Smith DR, Green C, Ranise S, Tinelli C, Ball T, Rajamani SK (2006) Intelligent systems and formal methods in software engineering. IEEE Intell Syst 21(6): 71\u201381","journal-title":"IEEE Intell Syst"},{"key":"73_CR11","doi-asserted-by":"crossref","unstructured":"B\u00e9rard B, Fribourg L (1999) Reachability analysis of (timed) petri nets using real arithmetic. In: Proceedings of 10th international conference on concurrency theory (CONCUR\u201999) LNCS 1664. Springer","DOI":"10.1007\/3-540-48320-9_14"},{"key":"73_CR12","doi-asserted-by":"crossref","unstructured":"Bertino E, Crampton J, Paci F (2006) Access control and authorization constraints for WS-BPEL. In: Proceedings of ICWS\u201906. IEEE Computer Society Press, pp 275\u2013284","DOI":"10.1109\/ICWS.2006.21"},{"key":"73_CR13","first-page":"118","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58: 118\u2013149","journal-title":"Adv Comput"},{"key":"73_CR14","doi-asserted-by":"crossref","unstructured":"Biere A, Heljanko K, Junttila TA, Latvala T, Schuppan V (2006) Linear encodings of bounded ltl model checking. Logical methods comput Sci 2(5)","DOI":"10.2168\/LMCS-2(5:5)2006"},{"issue":"1","key":"73_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/504909.504910","volume":"5","author":"P Bonatti","year":"2002","unstructured":"Bonatti P, di Vimercati SDC, Samarati P (2002) An algebra for composing access control policies. ACM Trans Inf Syst Secur 5(1): 1\u201335","journal-title":"ACM Trans Inf Syst Secur"},{"key":"73_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The classical decision problem","author":"E B\u00f6rger","year":"1997","unstructured":"B\u00f6rger E, Gr\u00e4del E, Gurevich Y (1997) The classical decision problem. Springer, Berlin"},{"key":"73_CR17","unstructured":"Bradley AR, Manna Z (2009) Property-directed incremental invariant generation. Formal aspects of computing. To appear"},{"key":"73_CR18","doi-asserted-by":"crossref","unstructured":"Calvi A, Ranise S, Vigan\u00f2 L (2010) Automated validation of security-sensitive web services specified in bpel and rbac. In: Proceedings of 1st workshop on software service (satellite of SYNASC symposium). Timisoara, Sept. 23\u201325 (2010). To appear in IEEE Comp. Society","DOI":"10.1109\/SYNASC.2010.75"},{"key":"73_CR19","volume-title":"Model theory","author":"C-C Chang","year":"1990","unstructured":"Chang C-C, Keisler JH (1990) Model theory. North-Holland, Amsterdam"},{"key":"73_CR20","unstructured":"Christensen E, Curbera F, Meredith G, Weerawarana S Web services description language (WSDL) 1.1. Available at http:\/\/www.w3.org\/TR\/wsdl"},{"key":"73_CR21","unstructured":"DeTreville J (2002) Binder, a logic-based security language. In: IEEE symposium on security and privacy. IEEE Computer Society Press"},{"key":"73_CR22","doi-asserted-by":"crossref","unstructured":"Deutsch A, Sui L, Vianu V, Zhou D (2006) Verification of Communicating data-driven web services. In: Proceedings of PODS\u201906. ACM Press","DOI":"10.1145\/1142351.1142364"},{"key":"73_CR23","doi-asserted-by":"crossref","unstructured":"Dougherty DJ, Fisler K, Krishnamurthi S (2006) Specifying and reasoning about dynamic access-control policies. In: Proceedings of IJCAR\u201906, LNCS 4130. Springer, pp 632\u2013646","DOI":"10.1007\/11814771_51"},{"key":"73_CR24","volume-title":"A mathematical introduction to logic","author":"HB Enderton","year":"1972","unstructured":"Enderton HB (1972) A mathematical introduction to logic. Academic Press, New York"},{"key":"73_CR25","doi-asserted-by":"crossref","unstructured":"Ernits J, Roo R, Jacky J, Veanes M (2009) Model-based testing of web applications using NModel. In: TESTCOM\/FATES. Springer-Verlag","DOI":"10.1007\/978-3-642-05031-2_14"},{"key":"73_CR26","doi-asserted-by":"crossref","unstructured":"Esparza J, Nielsen M (1994) Decidability issues for petri nets\u2014a survey. EATCS Bull (52)","DOI":"10.7146\/brics.v1i8.21662"},{"key":"73_CR27","unstructured":"Fast Home Page. http:\/\/www.lsv.ens-cachan.fr\/Software\/fast ."},{"key":"73_CR28","unstructured":"Ferraiolo D, Kuhn D (1992) Role-based access control. In: Proceedings of 15th NIST-NCSC national computer security conference. pp 554\u2013563"},{"key":"73_CR29","doi-asserted-by":"crossref","unstructured":"Fischer J, Majumdar R (2008) A theory of role composition. In: International conference on web services (ICWS \u201908). IEEE Comp. Society","DOI":"10.1109\/ICWS.2008.40"},{"key":"73_CR30","doi-asserted-by":"crossref","unstructured":"Flanagan C, Qaader S (2002) Predicate abstraction for software verification. In: Proceedings of the symposium on principles of programming languages (POPL\u201902). ACM Press, pp 191\u2013202","DOI":"10.1145\/503272.503291"},{"key":"73_CR31","doi-asserted-by":"crossref","unstructured":"Ge Y, de Moura L (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Proceedings of computer aided verification (CAV). pp 306\u2013320","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"73_CR32","doi-asserted-by":"crossref","unstructured":"Ghilardi S (2004) Model theoretic methods in combined constraint satisfiability. J Autom Reason 33(3\u20134)","DOI":"10.1007\/s10817-004-6241-5"},{"key":"73_CR33","doi-asserted-by":"crossref","unstructured":"Ghilardi S, Nicolini E, Ranise S, Zucchelli D (2008) Towards SMT model-checking of array-based Systems. In: Proceedings of the 4th international joint conference on automated reasoning (IJCAR 08). Springer, pp 67\u201382","DOI":"10.1007\/978-3-540-71070-7_6"},{"key":"73_CR34","doi-asserted-by":"crossref","unstructured":"Ghilardi S, Ranise S (2009) Goal directed invariant synthesis for model checking modulo theories. In: 18th international conference on automated reasoning with analytic tableaux and related methods (TABLEAUX 09). Springer, pp 173\u2013188","DOI":"10.1007\/978-3-642-02716-1_14"},{"key":"73_CR35","unstructured":"Gurevich Y, Neeman I Distributed-knowledge authorization language (DKAL). http:\/\/research.microsoft.com\/~gurevich\/DKAL.htm"},{"key":"73_CR36","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K Jensen","year":"2007","unstructured":"Jensen K, Kristensen L, Wells L (2007) Coloured petri nets and CPN tools for modelling and validation of concurrent systems. Int J Softw Tools Technol Transf 9: 213\u2013254","journal-title":"Int J Softw Tools Technol Transf"},{"key":"73_CR37","doi-asserted-by":"crossref","unstructured":"Lahiri SK, Bryant RE (2007) Predicate abstraction with indexed predicates. ACM Trans Comput Log 9(1)","DOI":"10.1145\/1297658.1297662"},{"issue":"1","key":"73_CR38","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/s10207-005-0073-0","volume":"5","author":"N Li","year":"2006","unstructured":"Li N, Mitchell JC (2006) Understanding SPKI\/SDSI using first-order logic. Int J Inf Secur 5(1): 48\u201364","journal-title":"Int J Inf Secur"},{"key":"73_CR39","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems: safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, New York"},{"issue":"3","key":"73_CR40","first-page":"23","volume":"31","author":"A Marconi","year":"2008","unstructured":"Marconi A, Pistore M, Traverso P (2008) Automated composition of web services: the astro approach. IEEE Data Eng Bull 31(3): 23\u201326","journal-title":"IEEE Data Eng Bull"},{"key":"73_CR41","unstructured":"OASIS business process execution language for Web Services specification V1.1. Available at. http:\/\/dev2dev.bea.com\/technologies\/webservices\/BPEL4WS.jsp"},{"key":"73_CR42","unstructured":"OASIS Committee draft (2007) Web services business process execution language v. 2.0"},{"issue":"3","key":"73_CR43","doi-asserted-by":"crossref","first-page":"20","DOI":"10.4018\/jwsr.2008070102","volume":"5","author":"F Paci","year":"2008","unstructured":"Paci F, Bertino E, Crampton J (2008) An access control framework for WS-BPEL. Int J Web Serv Res 5(3): 20\u201343","journal-title":"Int J Web Serv Res"},{"issue":"1","key":"73_CR44","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(91)90203-E","volume":"80","author":"W Reisig","year":"1991","unstructured":"Reisig W (1991) Petri nets and algebraic specifications. Theor Comput Sci 80(1): 1\u201334","journal-title":"Theor Comput Sci"},{"key":"73_CR45","unstructured":"Rybina T, Voronkov A (2003) A logical reconstruction of reachability. In: Proceedings of PSI\u201903, LNCS 2890. Springer, pp 222\u2013237"},{"key":"73_CR46","doi-asserted-by":"crossref","unstructured":"Schaad A, Moffett J, Jacob J (2001) The role-based access control system of a european bank: a case study and discussion. In: Proceedings of 6th ACM symposium on access control models and technologies. ACM Press","DOI":"10.1145\/373256.373257"},{"key":"73_CR47","unstructured":"Schaad A, Sohr K, Drouineaud M (2007) A workflow-based model-checking approach to inter- and intra-analysis of organisational controls in service-oriented business processes. J Inf Assur Secur 2(1)"},{"key":"73_CR48","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani R (2007) Lazy satisfiability modulo theories. J Satisfiability Boolean Model Comput 3: 141\u2013224","journal-title":"J Satisfiability Boolean Model Comput"},{"key":"73_CR49","unstructured":"Stahl C (2005) A petri net semantics for BPEL. Technical Report 188, Humbolt-Universit\u00e4t zu Berlin"},{"key":"73_CR50","doi-asserted-by":"crossref","unstructured":"Stoller SD, Yang P, Ramakrishnan C, Gofman MI (2007) Efficient policy analysis for administrative role-based access control. In: Proceedings of 20th IEEE computer security foundations workshop (CSFW)","DOI":"10.1145\/1315245.1315300"},{"key":"73_CR51","doi-asserted-by":"crossref","unstructured":"Tinelli C, Zarba CG (2005) Combining non-stably infinite theories. J Autom Reason 34(3)","DOI":"10.1007\/s10817-005-5204-9"},{"key":"73_CR52","unstructured":"Tools4bpel Home Page. http:\/\/www2.informatik.hu-berlin.de\/top\/tools4bpel"},{"key":"73_CR53","doi-asserted-by":"crossref","unstructured":"Tsai WT, Liu X, Chen Y (2005) Distributed policy specification and enforcement in service-oriented business systems. In: ICEBE \u201905: Proceedings of the IEEE international conference on e-business engineering. IEEE Computer Society, Washington, DC, USA, pp 10\u201317","DOI":"10.1109\/ICEBE.2005.52"},{"key":"73_CR54","doi-asserted-by":"crossref","unstructured":"Tsai WT, Liu X, Chen Y, Paul R (2005) Simulation verification and validation by dynamic policy enforcement. In: ANSS \u201905: Proceedings of the 38th annual Symposium on Simulation. IEEE Computer Society, Washington, DC, USA, pp 91\u201398","DOI":"10.1109\/ANSS.2005.42"},{"issue":"1","key":"73_CR55","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/s10257-007-0059-8","volume":"6","author":"W-T Tsai","year":"2008","unstructured":"Tsai W-T, Zhou X, Wei X (2008) A policy enforcement framework for verification and control of service collaboration. Inf Syst E-Bus Manag 6(1): 83\u2013107","journal-title":"Inf Syst E-Bus Manag"},{"issue":"1","key":"73_CR56","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"WMP Aalst van der","year":"1998","unstructured":"van der Aalst WMP (1998) The application of Petri nets to workflow management. J circuits syst comput 8(1): 21\u201366","journal-title":"J circuits syst comput"},{"key":"73_CR57","doi-asserted-by":"crossref","unstructured":"Veanes M, Bjoerner N, Raschke A (2008) An SMT approach to bounded reachability analysis of model programs. In: Proceedings of FORTE\u201908, LNCS 5048. Springer","DOI":"10.1007\/978-3-540-68855-6_4"},{"key":"73_CR58","unstructured":"Yices Home Page. http:\/\/yices.csl.sri.com"},{"key":"73_CR59","unstructured":"Z3 Home Page. http:\/\/research.microsoft.com\/en-us\/um\/redmond\/projects\/z3\/"},{"key":"73_CR60","doi-asserted-by":"crossref","unstructured":"Zhang N, Ryan MD, Guelev D (2005) Evaluating access control policies through model checking. In: Proceedings of ISC\u201905, LNCS 3650. Springer, pp 446\u2013460","DOI":"10.1007\/11556992_32"}],"container-title":["Service Oriented Computing and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11761-010-0073-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11761-010-0073-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11761-010-0073-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,15]],"date-time":"2020-06-15T02:14:56Z","timestamp":1592187296000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11761-010-0073-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,30]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["73"],"URL":"https:\/\/doi.org\/10.1007\/s11761-010-0073-4","relation":{},"ISSN":["1863-2386","1863-2394"],"issn-type":[{"value":"1863-2386","type":"print"},{"value":"1863-2394","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12,30]]}}}