{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T17:55:51Z","timestamp":1648922151157},"reference-count":21,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3650,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1016\/s1571-0661(04)80684-4","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"54-70","source":"Crossref","is-referenced-by-count":0,"title":["A formal approach for checking security properties in SecSpaces1 1Work partially supported by MEFISTO Progetto \u201cMetodi Formali per la Sicurezza e il Tempo\u201d and Microsoft Research Europe."],"prefix":"10.1016","volume":"85","author":[{"given":"Roberto","family":"Lucchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Bravetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Gorrieri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/S1571-0661(04)80684-4_NEWBIB1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2740","article-title":"A calculus for cryptographic protocols: The spi calculus","volume":"148","author":"Abadi","year":"1999","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB2","series-title":"1st International Workshop on Foundations of Coordination Languages and Software Architectures, volume 68.3 of ENTCS","article-title":"Secspaces: a data-driven coordination model for environments open to untrusted agents","author":"Busi","year":"2002"},{"issue":"2","key":"10.1016\/S1571-0661(04)80684-4_NEWBIB3","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/S0304-3975(97)00149-7","article-title":"A Process Algebraic View of Linda Coordination Primitives","volume":"192","author":"Busi","year":"1998","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB4","doi-asserted-by":"crossref","unstructured":"L. Bettini and R. De Nicola. A Java Middleware for Guaranteeing Privacy of Distributed Tuple Spaces. In Proc. of FIDJI'02, Int. Workshop on scientific engineering of distributed Java applications, 2002. To appear in LNCS.","DOI":"10.1007\/3-540-36520-6_16"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB5","unstructured":"Scientific Computing Associates. Linda: User's guide and reference manual. Scientific Computing Associates, 1995."},{"issue":"2","key":"10.1016\/S1571-0661(04)80684-4_NEWBIB6","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/129630.129635","article-title":"Coordination Languages and their Significance","volume":"35","author":"Carriero","year":"1992","journal-title":"Communications of the ACM"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB7","doi-asserted-by":"crossref","unstructured":"R. Focardi, R. Gorrieri, and F. Martinelli. Message Authentication through Non Interference. In Proc. of the 8th International Conference on Algebraic Methodology and Software Technology (AMAST '00), Lecture Notes in Computer Science 1816, Springer-Verlag, pp. 258\u2013272, Iowa City (USA), May 2000.","DOI":"10.1007\/3-540-45499-3_20"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB8","series-title":"International Colloquium on Automata, Languages and Programming (ICALP'00), volume 1853 of LNCS","article-title":"Non interference for the analysis of cryptographic protocols","author":"Focardi","year":"2000"},{"issue":"1","key":"10.1016\/S1571-0661(04)80684-4_NEWBIB9","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1145\/2363.2433","article-title":"Generative Communication in Linda","volume":"7","author":"Gelernter","year":"1985","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB10","series-title":"The Java Language Specification","author":"James","year":"1996"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB11","doi-asserted-by":"crossref","unstructured":"J.A. Goguen and J. Meseguer. Security Policies and Security Models. In Proc. of the IEEE Symposium on Security and Privacy, pages 11\u201320. IEEE Comp. Soc. Press., 1982.","DOI":"10.1109\/SP.1982.10014"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB12","doi-asserted-by":"crossref","unstructured":"Daniele Gorla and Rosario Pugliese. Resource Access and Mobility Control with Dynamic Privileges Acquisition. In Proc. of the Int. Colloquium on Automata, Languages and Programming (ICALP'03), LNCS, 2003. To appear.","DOI":"10.1007\/3-540-45061-0_11"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB13","doi-asserted-by":"crossref","unstructured":"Fabio Martinelli. Partial Model Checking and Theorem Proving for Ensuring Security Properties. In Proc. of the IEEE Computer Security Foundations Workshop (CSFW'98), pages 44\u201352. IEEE Comp. Soc. Press., 1998.","DOI":"10.1109\/CSFW.1998.683154"},{"issue":"1","key":"10.1016\/S1571-0661(04)80684-4_NEWBIB14","doi-asserted-by":"crossref","DOI":"10.1080\/08839510150204590","article-title":"Safe Tuplespace-Based Coordination in Multi Agent Systems","volume":"15","author":"Minsky","year":"2001","journal-title":"Journal of Applied Artificial Intelligence"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB15","doi-asserted-by":"crossref","unstructured":"R. De Nicola, G. Ferrari, and R. Pugliese. Coordinating Mobile Agents via Blackboards and Access Rights. In Proc. of the Second International Conference on Coordination Models and Languages, Lectures Notes in Computer Science 1282, Springer, pages 220\u2013237, 1997.","DOI":"10.1007\/3-540-63383-9_83"},{"issue":"5","key":"10.1016\/S1571-0661(04)80684-4_NEWBIB16","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1109\/32.685256","article-title":"KLAIM: A Kernel Language for Agents Interaction and Mobility","volume":"24","author":"De","year":"1998","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB17","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","article-title":"Testing equivalences for processes","volume":"34","author":"De","year":"1984","journal-title":"Theortical Computer Science"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB18","unstructured":"J. Pinakis. Providing directed communication in Linda. In Proceedings of the 15th Australian Computer Science Conference, pages 731\u2013743, 1992."},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB19","unstructured":"Sun Microsystems, Inc. JavaSpacesTM Service Specification, 2002. http:\/\/www.sun.com\/jini\/specs\/."},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB20","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/S0167-6423(02)00090-4","article-title":"Coordinating Processes with Secure Spaces","volume":"46","author":"Jan","year":"2003","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1571-0661(04)80684-4_NEWBIB21","article-title":"TSpaces","author":"Wyckoff","year":"1998","journal-title":"IBM System Journal"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806844?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806844?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:14:13Z","timestamp":1585898053000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104806844"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["S1571066104806844"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80684-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}