{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:13:39Z","timestamp":1746159219525,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642539961"},{"type":"electronic","value":"9783642539978"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-53997-8_1","type":"book-chapter","created":{"date-parts":[[2014,1,27]],"date-time":"2014-01-27T03:44:52Z","timestamp":1390794292000},"page":"1-11","source":"Crossref","is-referenced-by-count":2,"title":["Partial Model Checking for the Verification and Synthesis of Secure Service Compositions"],"prefix":"10.1007","author":[{"given":"Fabio","family":"Martinelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilaria","family":"Matteucci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Andersen, H.R.: Partial model checking. In: LICS, p. 398. IEEE (1995)","DOI":"10.1109\/LICS.1995.523274"},{"key":"1_CR2","unstructured":"Martinelli, F.: Languages for description and analysis of authentication protocols. In: Proceedings of 6th Italian Conference on Theoretical Computer Science, pp. 304\u2013315 (1998)"},{"issue":"1","key":"1_CR3","doi-asserted-by":"publisher","first-page":"1057","DOI":"10.1016\/S0304-3975(02)00596-0","volume":"290","author":"F. Martinelli","year":"2003","unstructured":"Martinelli, F.: Analysis of security protocols as open systems. TCS\u00a0290(1), 1057\u20131106 (2003)","journal-title":"TCS"},{"key":"1_CR4","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Ciancia, V., Martin, J.A., Martinelli, F., Matteucci, I., Petrocchi, M., Pimentel, E.: A tool for the synthesis of cryptographic orchestrators. In: Model Driven Security Workshop, MDSEC. ACM (2012)","DOI":"10.1145\/2422498.2422508"},{"key":"1_CR6","unstructured":"Martinelli, F.: Formal Methods for the Analysis of Open Systems with Applications to Security Properties. PhD thesis, University of Siena (1998)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-49059-0_11","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"D. Marchignoli","year":"1999","unstructured":"Marchignoli, D., Martinelli, F.: Automatic verification of cryptographic protocols through compositional analysis techniques. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 148\u2013162. Springer, Heidelberg (1999)"},{"issue":"1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1002\/stvr.329","volume":"16","author":"F. Martinelli","year":"2006","unstructured":"Martinelli, F., Petrocchi, M., Vaccarelli, A.: Formal analysis of some secure procedures for certificate delivery. Softw. Test., Verif. Reliab.\u00a016(1), 33\u201359 (2006)","journal-title":"Softw. Test., Verif. Reliab."},{"key":"1_CR9","unstructured":"Ciancia, V., Martinelli, F., Matteucci, I., Morisset, C.: Quantitative evaluation of enforcement strategies. In: Proceedings of FPS 2013. LNCS, vol.\u00a08352 (2013)"},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2004.02.023","volume":"105","author":"M. Baldoni","year":"2004","unstructured":"Baldoni, M., Baroglio, C., Martelli, A., Patti, V.: Reasoning about interaction protocols for web service composition. Electr. Notes Theor. Comput. Sci.\u00a0105, 21\u201336 (2004)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"1_CR11","unstructured":"Bao, L., Zhang, W., Zhang, X.: Describing and Verifying Web Service Using CCS. In: PDCAT"},{"issue":"1","key":"1_CR12","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/j.entcs.2005.12.038","volume":"154","author":"J. C\u00e1mara","year":"2006","unstructured":"C\u00e1mara, J., Canal, C., Cubo, J., Vallecillo, A.: Formalizing wsbpel business processes using process algebra. Electr. Notes Theor. Comput. Sci.\u00a0154(1), 159\u2013173 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Ferrara, A.: Web services: a process algebra approach. In: Aiello, M., Aoyama, M., Curbera, F., Papazoglou, M.P. (eds.) ICSOC, pp. 242\u2013251. ACM (2004)","DOI":"10.1145\/1035167.1035202"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1109\/ICWS.2004.1314722","volume-title":"Proceedings of the IEEE International Conference on Web Services (ICWS 2004)","author":"G. Salaun","year":"2004","unstructured":"Salaun, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: Proceedings of the IEEE International Conference on Web Services (ICWS 2004), p. 43. IEEE Computer Society, Washington, DC (2004)"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/11494881_16","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"W. Reisig","year":"2005","unstructured":"Reisig, W.: Modeling- and analysis techniques for web services and business processes. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol.\u00a03535, pp. 243\u2013258. Springer, Heidelberg (2005)"},{"key":"1_CR16","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: Plans for service composition. In: Workshop on Issues in the Theory of Security, WITS (2006)"},{"key":"1_CR17","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: Types and effects for secure service orchestration. In: Proc. 19th Computer Security Foundations Workshop, CSFW (2006)"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11768869_1","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"M. Bartoletti","year":"2006","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: Security issues in service composition. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol.\u00a04037, pp. 1\u201316. Springer, Heidelberg (2006)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/11431053_5","volume-title":"The Semantic Web: Research and Applications","author":"M. Pistore","year":"2005","unstructured":"Pistore, M., Roberti, P., Traverso, P.: Process-level composition of executable web services: \u201cOn-the-fly\u201d versus \u201cOnce-for-all\u201d composition. In: G\u00f3mez-P\u00e9rez, A., Euzenat, J. (eds.) ESWC 2005. LNCS, vol.\u00a03532, pp. 62\u201377. Springer, Heidelberg (2005)"},{"key":"1_CR20","unstructured":"Pistore, M., Traverso, P., Bertoli, P.: Automated composition of web services by planning in asynchronous domains. In: Biundo, S., Myers, K.L., Rajan, K. (eds.) ICAPS, pp. 2\u201311. AAAI (2005)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/11596141_18","volume-title":"Service-Oriented Computing - ICSOC 2005","author":"N. Busi","year":"2005","unstructured":"Busi, N., Gorrieri, R., Guidi, C., Lucchi, R., Zavattaro, G.: Choreography and orchestration: A synergic approach for system design. In: Benatallah, B., Casati, F., Traverso, P. (eds.) ICSOC 2005. LNCS, vol.\u00a03826, pp. 228\u2013240. Springer, Heidelberg (2005)"},{"key":"1_CR22","first-page":"123","volume-title":"Proceedings of the 17th ACM Symposium on Access Control Models and Technologies, SACMAT 2012","author":"A.D. Brucker","year":"2012","unstructured":"Brucker, A.D., Hang, I., L\u00fcckemeyer, G., Ruparel, R.: Securebpmn: modeling and enforcing access control requirements in business processes. In: Proceedings of the 17th ACM Symposium on Access Control Models and Technologies, SACMAT 2012, pp. 123\u2013126. ACM, New York (2012)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71316-6_4","volume-title":"Programming Languages and Systems","author":"A. Lapadula","year":"2007","unstructured":"Lapadula, A., Pugliese, R., Tiezzi, F.: A calculus for orchestration of web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 33\u201347. Springer, Heidelberg (2007)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-642-19125-1_3","volume-title":"Engineering Secure Software and Systems","author":"W. Arsac","year":"2011","unstructured":"Arsac, W., Compagna, L., Pellegrino, G., Ponta, S.E.: Security validation of business processes via model-checking. In: Erlingsson, \u00da., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol.\u00a06542, pp. 29\u201342. Springer, Heidelberg (2011)"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Martinelli, F., Matteucci, I.: A framework for automatic generation of security controller. STVR (2010)","DOI":"10.1002\/stvr.441"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/3-540-59042-0_76","volume-title":"STACS 95","author":"O. Maler","year":"1995","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol.\u00a0900, pp. 229\u2013242. Springer, Heidelberg (1995)"},{"issue":"2","key":"1_CR27","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/j.jlap.2011.08.001","volume":"81","author":"J.A. Mart\u00edn","year":"2012","unstructured":"Mart\u00edn, J.A., Martinelli, F., Pimentel, E.: Synthesis of secure adaptors. J. Log. Algebr. Program.\u00a081(2), 99\u2013126 (2012)","journal-title":"J. Log. Algebr. Program."},{"issue":"3-5","key":"1_CR28","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1016\/j.jlap.2010.07.001","volume":"80","author":"J.A. Mart\u00edn","year":"2011","unstructured":"Mart\u00edn, J.A., Pimentel, E.: Contracts for security adaptation. J. Log. Algebr. Program.\u00a080(3-5), 154\u2013179 (2011)","journal-title":"J. Log. Algebr. Program."},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Mekki, M.A., Rusinowitch, M.: Automatic composition of services with security policies. In: IEEE SERVICES 2008 - Part I, pp. 529\u2013537 (2008)","DOI":"10.1109\/SERVICES-1.2008.13"},{"key":"1_CR30","first-page":"69","volume":"155","author":"L. Vigan\u00f2","year":"2006","unstructured":"Vigan\u00f2, L.: Automated security protocol analysis with the AVISPA tool. ENTCS\u00a0155, 69\u201386 (2006)","journal-title":"ENTCS"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-28756-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Armando","year":"2012","unstructured":"Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 267\u2013282. Springer, Heidelberg (2012)"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Li, J., Yarvis, M., Reiher, P.: Securing distributed adaptation. Computer Networks 38(3) (2002)","DOI":"10.1016\/S1389-1286(01)00291-2"}],"container-title":["Lecture Notes in Computer Science","Public Key Infrastructures, Services and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-53997-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T17:30:15Z","timestamp":1746120615000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-53997-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642539961","9783642539978"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-53997-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}