乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:24:10Z","timestamp":1720625050687},"reference-count":36,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2005,2,1]],"date-time":"2005-02-01T00:00:00Z","timestamp":1107216000000},"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":3100,"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":[[2005,2]]},"DOI":"10.1016\/j.entcs.2004.10.006","type":"journal-article","created":{"date-parts":[[2005,2,11]],"date-time":"2005-02-11T14:16:45Z","timestamp":1108131405000},"page":"23-46","source":"Crossref","is-referenced-by-count":2,"special_numbering":"C","title":["A Coordination-based Methodology for Security Protocol Verification"],"prefix":"10.1016","volume":"121","author":[{"given":"Giacomo","family":"Baldi","sequence":"first","affiliation":[]},{"given":"Andrea","family":"Bracciali","sequence":"additional","affiliation":[]},{"given":"Gianluigi","family":"Ferrari","sequence":"additional","affiliation":[]},{"given":"Emilio","family":"Tuosto","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/j.entcs.2004.10.006_bib001","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\/j.entcs.2004.10.006_bib002","unstructured":"R. Amadio, D. Lugiez, and V. Vancack\u00e9re. On the symbolic reduction of processes with cryptographic functions. Technical report, INRIA-Sophia, 2001"},{"key":"10.1016\/j.entcs.2004.10.006_bib003","series-title":"Proc. COORDINATION 2002","article-title":"Coordination for orchestration","volume":"volume 2315","author":"Andrade","year":"2002"},{"key":"10.1016\/j.entcs.2004.10.006_bib004","series-title":"WITS'04","article-title":"Control flow analysis can find new flaws too","author":"Bodei","year":"2004"},{"key":"10.1016\/j.entcs.2004.10.006_bib005","series-title":"ICALP","article-title":"Symbolic trace analysis of cryptographic protocols","author":"Boreale","year":"2001"},{"key":"10.1016\/j.entcs.2004.10.006_bib006","series-title":"CONCUR: 13th International Conference on Concurrency Theory","article-title":"A framework for the analysis of security protocols","author":"Boreale","year":"2002"},{"key":"10.1016\/j.entcs.2004.10.006_bib007","series-title":"Proc. of PDPTA02","article-title":"Security and dynamic composition of open systems","author":"Bracciali","year":"2002"},{"key":"10.1016\/j.entcs.2004.10.006_bib008","unstructured":"A. Bracciali, A. Brogi, and F. Turini. A framework for specifying and verfying the behaviour of open systems. The Journal of Logic and Algebraic Programming. Special Issue on Process Algebra and System Architecture. Elsevier. To appear"},{"key":"10.1016\/j.entcs.2004.10.006_bib009","unstructured":"A. Bracciali. Behavioural Patterns and Software Composition. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, 2003"},{"issue":"1","key":"10.1016\/j.entcs.2004.10.006_bib010","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/77648.77649","article-title":"A logic of authentication","volume":"8","author":"Burrows","year":"1990","journal-title":"ACM Transactions on Computer Systems"},{"issue":"2","key":"10.1016\/j.entcs.2004.10.006_bib011","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\/j.entcs.2004.10.006_bib012","series-title":"Proc. of CSFW","article-title":"Relating strands and multiset rewriting for security protocol analysis","author":"Cervesato","year":"2000"},{"key":"10.1016\/j.entcs.2004.10.006_bib013","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, S. Jha, and W.R. Marrero. Using state space exploration and a nautural deduction style message derivation engine to verify security protocols. In In Proc. IFIP PROCOMET, 1998","DOI":"10.1007\/978-0-387-35358-6_10"},{"issue":"4","key":"10.1016\/j.entcs.2004.10.006_bib014","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","article-title":"Formal methods: State of the art and future directions","volume":"28","author":"Clarke","year":"1996","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/j.entcs.2004.10.006_bib015","series-title":"Proc. of the 8th ACM conference on Computer and Communications Security","article-title":"Events in security protocols","author":"Crazzolara","year":"2001"},{"issue":"10","key":"10.1016\/j.entcs.2004.10.006_bib016","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1145\/944217.944234","article-title":"The next step in web services","volume":"46","author":"Curbera","year":"2003","journal-title":"Communications of the ACM"},{"key":"10.1016\/j.entcs.2004.10.006_bib017","article-title":"On the security of public key protocols","volume":"29","author":"Dolev","year":"1983","journal-title":"IEEETIT: IEEE Transactions on Information Theory"},{"issue":"4","key":"10.1016\/j.entcs.2004.10.006_bib018","first-page":"269","article-title":"Introduction to the special issue on software architecture","volume":"21","author":"Garlan","year":"1995","journal-title":"Software Engineering"},{"key":"10.1016\/j.entcs.2004.10.006_bib019","unstructured":"A. Kehne, J. Sch\u00f6nw\u00e4lder, and H. Langend\u00f6rfer. Multiple authentications with a nonce-based protocol using generalized timestamps. In Proc. ICCC '92, 1992"},{"key":"10.1016\/j.entcs.2004.10.006_bib020","doi-asserted-by":"crossref","unstructured":"J. Kohl and B. Neuman. The kerberos network authentication service (version 5). Internet Request for Comment RFC-1510, 1993","DOI":"10.17487\/rfc1510"},{"key":"10.1016\/j.entcs.2004.10.006_bib021","series-title":"TACAS","article-title":"Breaking and fixing the Needham-Schroeder public-key protocol using FDR","volume":"volume 1055","author":"Lowe","year":"1996"},{"issue":"1","key":"10.1016\/j.entcs.2004.10.006_bib022","doi-asserted-by":"crossref","first-page":"1057","DOI":"10.1016\/S0304-3975(02)00596-0","article-title":"Analysis of security protocols as open systems","volume":"209","author":"Martinelli","year":"2003","journal-title":"TCS"},{"key":"10.1016\/j.entcs.2004.10.006_bib023","series-title":"Handbook of Applied Cryptography","author":"Menzies","year":"1997"},{"key":"10.1016\/j.entcs.2004.10.006_bib024","doi-asserted-by":"crossref","unstructured":"J.K. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In ACM Conference on Computer and Communications Security, 2001","DOI":"10.1145\/501983.502007"},{"issue":"1","key":"10.1016\/j.entcs.2004.10.006_bib025","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes, I and II","volume":"100","author":"Milner","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/j.entcs.2004.10.006_bib026","series-title":"10th IEEE Computer Security Foundations Workshop","article-title":"Automated analysis of cryptographic protocols using mur\u03d5","author":"Mitchell","year":"1997"},{"issue":"2","key":"10.1016\/j.entcs.2004.10.006_bib027","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1145\/155848.155852","article-title":"A note on the use of timestamps as nonces","volume":"27","author":"Neumann","year":"1993","journal-title":"Operating Systems Review"},{"key":"10.1016\/j.entcs.2004.10.006_bib028","unstructured":"L.C. Paulson. The inductive approach to verifying cryptographic protocols. Technical report; no. 443. 4006797499. University of Cambridge Computer Laboratory, Cambridge, UK, USA, February 1998"},{"key":"10.1016\/j.entcs.2004.10.006_bib029","series-title":"Proc. of CSFW","article-title":"Proving properties of security protocols by induction","author":"Paulson","year":"1997"},{"key":"10.1016\/j.entcs.2004.10.006_bib030","unstructured":"M. Shaw. Architectural Requirements for Computing with Coalitions of Resources, 1999. Position paper for First Working IFIP Conference on Software Architecture"},{"issue":"1,2","key":"10.1016\/j.entcs.2004.10.006_bib031","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","article-title":"Athena, a novel approach to efficient automatic security protocol analysis","volume":"9","author":"Song","year":"2001","journal-title":"Computer Security"},{"key":"10.1016\/j.entcs.2004.10.006_bib032","series-title":"Cryptography: Theory and practice","author":"Stinson","year":"1995"},{"key":"10.1016\/j.entcs.2004.10.006_bib033","unstructured":"J. Thayer, J. Herzog, and J. Guttman. Honest ideals on strand spaces. In 11th IEEE Computer Security Foundations Workshop, 1998"},{"issue":"2,3","key":"10.1016\/j.entcs.2004.10.006_bib034","first-page":"181","article-title":"Strand spaces: Proving security protocols correct","volume":"7","author":"Thayer","year":"1999","journal-title":"Journal of Computer Security"},{"key":"10.1016\/j.entcs.2004.10.006_bib035","unstructured":"E. Tuosto. Non-Functional Aspects of Wide Area Network Programming. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, 2003"},{"key":"10.1016\/j.entcs.2004.10.006_bib036","unstructured":"V. Vanack\u00e9re. The trust protocol analyser. automatic and efficient verification of cryptographic protocols. In VERIFY02, 2002"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610500023X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610500023X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T19:26:54Z","timestamp":1586114814000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610500023X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,2]]},"references-count":36,"alternative-id":["S157106610500023X"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2004.10.006","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2005,2]]}}}