乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,8]],"date-time":"2023-01-08T16:50:48Z","timestamp":1673196648189},"reference-count":37,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2005,6,1]],"date-time":"2005-06-01T00:00:00Z","timestamp":1117584000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3004,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2005,6]]},"DOI":"10.1016\/j.tcs.2005.03.044","type":"journal-article","created":{"date-parts":[[2005,4,13]],"date-time":"2005-04-13T17:01:38Z","timestamp":1113411698000},"page":"393-425","source":"Crossref","is-referenced-by-count":10,"title":["A method for symbolic analysis of security protocols"],"prefix":"10.1016","volume":"338","author":[{"given":"Michele","family":"Boreale","sequence":"first","affiliation":[]},{"given":"Maria Grazia","family":"Buscemi","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2005.03.044_bib1","doi-asserted-by":"crossref","unstructured":"M. Abadi, C. Fournet, Mobile values, new names, and secure communication, in: Conf. Rec. of POPL\u201901, 2001.","DOI":"10.1145\/360204.360213"},{"key":"10.1016\/j.tcs.2005.03.044_bib2","doi-asserted-by":"crossref","unstructured":"R.M. Amadio, S. Lugiez, On the reachability problem in cryptographic protocols, in: Proc. of Concur\u201900, Lecture Notes in Computer Science, Vol. 1877, Springer, Berlin, 2000.","DOI":"10.1007\/3-540-44618-4_28"},{"issue":"1","key":"10.1016\/j.tcs.2005.03.044_bib3","doi-asserted-by":"crossref","first-page":"695","DOI":"10.1016\/S0304-3975(02)00090-7","article-title":"On the symbolic reduction of processes with cryptographic functions","volume":"290","author":"Amadio","year":"2003","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.tcs.2005.03.044_bib4","unstructured":"R. Amadio, S. Prasad, The game of the name in cryptographic tables, in: Proc. of Asian\u201900, Lecture Notes in Computer Science, Vol. 1742, Springer, Berlin, 2000. RR 3733 INRIA Sophia Antipolis."},{"key":"10.1016\/j.tcs.2005.03.044_bib5","series-title":"Proc. of 14th Computer Security Foundations Workshop","article-title":"An efficient cryptographic protocol verifier based on prolog rules","author":"Blanchet","year":"2001"},{"key":"10.1016\/j.tcs.2005.03.044_bib6","doi-asserted-by":"crossref","unstructured":"B. Blanchet, A. Podelski, Verification of cryptographic protocols: tagging enforces termination, in: Proc. of FoSSaCS\u201903, Lecture Notes in Computer Science, vol. 2620, Springer, Berlin, 2003.","DOI":"10.1007\/3-540-36576-1_9"},{"key":"10.1016\/j.tcs.2005.03.044_bib7","doi-asserted-by":"crossref","unstructured":"M. Boreale, Symbolic trace analysis of cryptographic protocols, in: Proc. of ICALP\u201901, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001.","DOI":"10.1007\/3-540-48224-5_55"},{"key":"10.1016\/j.tcs.2005.03.044_bib8","series-title":"Proc. of SAC\u201902","article-title":"Experimenting with STA, a tool for automatic analysis of security protocols","author":"Boreale","year":"2002"},{"key":"10.1016\/j.tcs.2005.03.044_bib9","doi-asserted-by":"crossref","unstructured":"M. Boreale, M. Buscemi, A framework for the analysis of security protocol, in: Proc. of CONCUR \u201902, Lecture Notes in Computer Science, Vol. 2421, Springer, Berlin, 2002.","DOI":"10.1007\/3-540-45694-5_32"},{"key":"10.1016\/j.tcs.2005.03.044_bib10","series-title":"Proc. of LICS\u201903","article-title":"An NP decision procedure for protocol insecurity with Xor","author":"Chevalier","year":"2003"},{"key":"10.1016\/j.tcs.2005.03.044_bib11","doi-asserted-by":"crossref","unstructured":"Y. Chevalier, R. Kuesters, M. Rusinowitch, M. Turuani, Deciding the security of protocols with Diffie\u2013Hellman exponentiation and product in exponents, in: Proc. of FSTTCS\u201903, Lecture Notes in Computer Science, Vol. 2914, Springer, Berlin, 2003.","DOI":"10.1007\/978-3-540-24597-1_11"},{"key":"10.1016\/j.tcs.2005.03.044_bib12","doi-asserted-by":"crossref","unstructured":"H. Comon, V. Cortier, J. Mitchell, Tree automata with one memory, set constraints and ping-pong protocols, in: Proc. of ICALP\u201901, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001.","DOI":"10.1007\/3-540-48224-5_56"},{"key":"10.1016\/j.tcs.2005.03.044_bib13","doi-asserted-by":"crossref","unstructured":"H. Comon-Lundh, V. Cortier, New decidability results for fragments of first-order logic and application to cryptographic protocols, in: Proc. of RTA\u201903, Lecture Notes in Computer Science, Vol. 2706, Springer, Berlin, 2003.","DOI":"10.1007\/3-540-44881-0_12"},{"key":"10.1016\/j.tcs.2005.03.044_bib14","series-title":"Proc. LICS \u201903","article-title":"Intruder deductions, constraint solving and insecurity decision in presence of exclusive or","author":"Comon-Lundh","year":"2003"},{"issue":"29","key":"10.1016\/j.tcs.2005.03.044_bib15","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public-key protocols","volume":"2","author":"Dolev","year":"1983","journal-title":"IEEE Trans. Inform. Theory"},{"key":"10.1016\/j.tcs.2005.03.044_bib16","series-title":"Proc. of Workshop on Formal Methods and Security Protocols","article-title":"Undecidability of bounded security protocols","author":"Durgin","year":"1999"},{"key":"10.1016\/j.tcs.2005.03.044_bib17","series-title":"Proc. of FOCS","article-title":"On the security of multi-party ping-pong protocols","author":"Even","year":"1983"},{"key":"10.1016\/j.tcs.2005.03.044_bib18","series-title":"Proc. of 14th Computer Security Foundations Workshop","article-title":"Computing symbolic models for verifying cryptographic protocols","author":"Fiore","year":"2001"},{"key":"10.1016\/j.tcs.2005.03.044_bib19","series-title":"Proc. of 13th Computer Security Foundations Workshop","article-title":"How to prevent type flaw attacks on security protocols","author":"Heather","year":"2000"},{"issue":"1","key":"10.1016\/j.tcs.2005.03.044_bib20","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1109\/32.481514","article-title":"A model for secure protocols and their compositions","volume":"22","author":"Heintze","year":"1996","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/j.tcs.2005.03.044_bib21","series-title":"Proc. of Workshop on Formal Methods and Security Protocols","article-title":"Efficient infinite-state analysis of security protocols","author":"Huima","year":"1999"},{"key":"10.1016\/j.tcs.2005.03.044_bib22","series-title":"Foundations of Logic Programming","author":"Lloyd","year":"1987"},{"key":"10.1016\/j.tcs.2005.03.044_bib23","doi-asserted-by":"crossref","unstructured":"G. Lowe, Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR, in: Proc. of TACAS\u201996, Lecture Notes in Computer Science, Vol. 1055, Springer, Berlin, 1996.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"10.1016\/j.tcs.2005.03.044_bib24","series-title":"Proc. of 10th IEEE Computer Security Foundations Workshop","article-title":"A hierarchy of authentication specifications","author":"Lowe","year":"1997"},{"key":"10.1016\/j.tcs.2005.03.044_bib25","series-title":"Handbook of Applied Cryptography","author":"Menezes","year":"1996"},{"key":"10.1016\/j.tcs.2005.03.044_bib26","series-title":"Proc. of 8th ACM Conf. on Computer and Communication Security","article-title":"Constraint solving for bounded-process cryptographic protocol analysis","author":"Millen","year":"2001"},{"key":"10.1016\/j.tcs.2005.03.044_bib27","series-title":"Proc. of the 14th IEEE Computer Security Foundations Workshop","article-title":"A security analysis of the cliques protocols suites","author":"Pereira","year":"2001"},{"key":"10.1016\/j.tcs.2005.03.044_bib28","series-title":"Proc. of Symp. Security and Privacy","article-title":"Automated analysis of cryptographic protocols using mur\u03d5","author":"Mitchell","year":"1997"},{"key":"10.1016\/j.tcs.2005.03.044_bib29","doi-asserted-by":"crossref","unstructured":"R. Ramanujam, S.P. Suresh, Tagging makes secrecy decidable for unbounded nonces as well, in: Proc. of FST&TCS\u201903, Lecture Notes in Computer Science, Vol. 2914, Springer, Berlin, 2003.","DOI":"10.1007\/978-3-540-24597-1_31"},{"key":"10.1016\/j.tcs.2005.03.044_bib30","unstructured":"R. Ramanujam, S.P. Suresh, A decidable subclass of unbounded security protocols, in WITS\u201903, 2003."},{"key":"10.1016\/j.tcs.2005.03.044_bib31","unstructured":"R. Ramanujam, S.P. Suresh, Undecidability of secrecy for security protocols. Manuscript, 2003. Available at http:\/\/www.imsc.res.in\/\u223cjam\/TR-undec.ps.gz."},{"key":"10.1016\/j.tcs.2005.03.044_bib32","series-title":"Proc. of 8th Computer Security Foundations Workshop","article-title":"Modelling and verifying key-exchange using CSP and FDR","author":"Roscoe","year":"1995"},{"issue":"1\u20133","key":"10.1016\/j.tcs.2005.03.044_bib33","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1016\/S0304-3975(02)00490-5","article-title":"Protocol insecurity with finite number of sessions in NP-complete","volume":"299","author":"Rusinowitch","year":"2003","journal-title":"Theoret. Comput. Sci."},{"issue":"8","key":"10.1016\/j.tcs.2005.03.044_bib34","first-page":"743","article-title":"Verifying authentication protocols in CSP","volume":"24","author":"Schneider","year":"1998","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/j.tcs.2005.03.044_bib35","doi-asserted-by":"crossref","unstructured":"V. Shmatikov. Decidable analysis of cryptographic protocols with products and modular exponentiation, in: Proc. of ESOP \u201904, Lecture Notes in Computer Science, Vol. 2986, Springer, Berlin, 2004.","DOI":"10.1007\/978-3-540-24725-8_25"},{"key":"10.1016\/j.tcs.2005.03.044_bib36","unstructured":"STA: a tool for trace analysis of cryptographic protocols. ML object code and examples, 2001. Available at http:\/\/www.dsi.unifi.it\/\u223cboreale\/tool.html. Online version at http:\/\/jordie.di.unipi.it:8080\/pweb."},{"issue":"1","key":"10.1016\/j.tcs.2005.03.044_bib37","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","article-title":"Strand spaces: proving security protocols correct","volume":"7","author":"Thayer","year":"1999","journal-title":"J. Comput. Security"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397505001659?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397505001659?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,12]],"date-time":"2019-02-12T07:15:08Z","timestamp":1549955708000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397505001659"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,6]]},"references-count":37,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2005,6]]}},"alternative-id":["S0304397505001659"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2005.03.044","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2005,6]]}}}