{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:22:35Z","timestamp":1720624955757},"reference-count":37,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2001,11,1]],"date-time":"2001-11-01T00:00:00Z","timestamp":1004572800000},"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":4288,"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":[[2001,11]]},"DOI":"10.1016\/s1571-0661(04)80968-x","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"280-310","source":"Crossref","is-referenced-by-count":21,"special_numbering":"C","title":["A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols"],"prefix":"10.1016","volume":"45","author":[{"given":"J.","family":"Mitchell","sequence":"first","affiliation":[]},{"given":"A.","family":"Ramanathan","sequence":"additional","affiliation":[]},{"given":"A.","family":"Scedrov","sequence":"additional","affiliation":[]},{"given":"V.","family":"Teague","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB1","doi-asserted-by":"crossref","unstructured":"M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In 28th ACM Symposium on Principles of Programming Languages, pages 104\u2013115, 2001.","DOI":"10.1145\/360204.360213"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB2","doi-asserted-by":"crossref","unstructured":"M. Abadi and A. Gordon. A bisimulation method for cryptographic protocol. In Proc. ESOP'98, Springer Lecture Notes in Computer Science, 1998.","DOI":"10.1007\/BFb0053560"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB3","doi-asserted-by":"crossref","unstructured":"M. Abadi and A. Gordon. A calculus for cryptographic protocols: the spi calculus. Information and Computation, 143:1\u201370, 1999. Expanded version available as SRC Research Report 149 (January 1998).","DOI":"10.1006\/inco.1998.2740"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB4","doi-asserted-by":"crossref","unstructured":"M. Abadi, and J. J\u00fcrjens. Formal eavesdropping and its computational interpretation. In Proc. 4-th International Symposium on Theoretical Aspects of Computer Software (TACS2001), Tohoku University, Sendai, Japan, 2001. Springer LNCS.","DOI":"10.1007\/3-540-45500-0_4"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB5","unstructured":"M. Abadi and P. Rogaway. Reconciling two views of cryptography (The computational soundness of formal encryption). In IFIP International Conference on Theoretical Computer Science, Sendai, Japan, 2000. Full paper to appear in J. of Cryptology."},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB6","series-title":"Algorithms and Theory of Computation Handbook","first-page":"19","year":"1999"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB7","doi-asserted-by":"crossref","unstructured":"S. Bellantoni. Predicative Recursion and Computational Complexity. PhD thesis, University of Toronto, 1992.","DOI":"10.1007\/BF01201998"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB8","doi-asserted-by":"crossref","unstructured":"M. Burrows, M. Abadi, and R. Needham. A logic of authentication. Proceedings of the Royal Society, Series A, 426(1871):233\u2013271, 1989. Also appeared as SRC Research Report 39 and, in a shortened form, in ACM Transactions on Computer Systems 8, 1 (February 1990), 18\u201336.","DOI":"10.1145\/77648.77649"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB9","doi-asserted-by":"crossref","unstructured":"R. Canetti. A unified framework for analyzing security of protocols. Cryptology ePrint Archive: Report 2000\/067; see http:\/\/eprint.iacr.org\/2000\/067\/, 2000.","DOI":"10.1007\/s001459910006"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB10","series-title":"12-th IEEE Computer Security Foundations Workshop","article-title":"A metanotation for protocol analysis","author":"Cervesato","year":"1999"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB11","doi-asserted-by":"crossref","unstructured":"D. Dolev, C. Dwork, and M. Naor. Non-malleable cryptography (extended abstract). In Proc. 23rd Annual ACM Symposium on the Theory of Computing, pages 542\u2013552, 1991.","DOI":"10.1145\/103418.103474"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB12","doi-asserted-by":"crossref","unstructured":"D. Dolev and A. Yao. On the security of public-key protocols. In Proc. 22nd Annual IEEE Symp. Foundations of Computer Science, pages 350\u2013357, 1981.","DOI":"10.1109\/SFCS.1981.32"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB13","article-title":"A compositional logic for protocol correctness","author":"Durgin","year":"2001","journal-title":"IEEE Computer Security Foundations Workshop"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB14","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1109\/TIT.1985.1057074","article-title":"A public-key cryptosystem and a signature scheme based on discrete logarithms","volume":"IT-31","author":"ElGamal","year":"1985","journal-title":"IEEE Transactions on Information Theory"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB15","doi-asserted-by":"crossref","unstructured":"R. Gennaro. An improved pseudo-random generator based on discrete log. In Proc. CRYPTO 2000, pages 469\u2013481. Springer LNCS 1880, 2000. Revised version available on www.research.ibm.com\/people\/r\/rosario\/.","DOI":"10.1007\/3-540-44598-6_29"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB16","series-title":"Modern Cryptography, Probabilistic Proofs and Pseudo-randomness","author":"Goldreich","year":"1999"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB17","unstructured":"O. Goldreich. The Foundations of Cryptography \u2013- A Book in Preparation. Available on www.wisdom.weizmann.ac.il\/~oded\/foc-book.html, 2000."},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB18","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/0022-0000(84)90070-9","article-title":"Probabilistic encryption","volume":"28","author":"Goldwasser","year":"1984","journal-title":"J. Computer and System Sciences"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB19","doi-asserted-by":"crossref","unstructured":"M. Hofmann. Type systems for polynomial-time computation. Habilitation thesis, Darmstadt, 1999; see www.dcs.ed.ac.uk\/home\/mxh\/papers.html, 1999.","DOI":"10.1109\/LICS.1999.782641"},{"issue":"2","key":"10.1016\/S1571-0661(04)80968-X_NEWBIB20","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00197942","article-title":"Three systems for cryptographic protocol analysis","volume":"7","author":"Kemmerer","year":"1994","journal-title":"J. Cryptology"},{"issue":"1","key":"10.1016\/S1571-0661(04)80968-X_NEWBIB21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","article-title":"Bisimulation through probabilistic testing","volume":"94","author":"Larsen","year":"1991","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB22","first-page":"776","article-title":"Probabilistic polynomial-time equivalence and security protocols","volume":"Vol. I","author":"Lincoln","year":"1999"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB23","doi-asserted-by":"crossref","unstructured":"P.D. Lincoln, M. Mitchell, J.C. Mitchell, and A. Scedrov. A probabilistic poly-time framework for protocol analysis. In M.K. Reiter, editor, Proc. 5-th ACM Conference on Computer and Communications Security, pages 112\u2013121, San Francisco, California, 1998. ACM Press.","DOI":"10.1145\/288090.288117"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB24","doi-asserted-by":"crossref","unstructured":"G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In 2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB25","series-title":"Pseudorandomness and Cryptographic","author":"Luby","year":"1996"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB26","doi-asserted-by":"crossref","unstructured":"C. Meadows. Analyzing the Needham-Schroeder public-key protocol: a comparison of two approaches. In Proc. European Symposium On Research In Computer Security. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61770-1_46"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB27","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB28","doi-asserted-by":"crossref","unstructured":"J.C. Mitchell, M. Mitchell, and A. Scedrov. A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In Proc. 39-th Annual IEEE Symposium on Foundations of Computer Science, pages 725\u2013733, Palo Alto, California, 1998. IEEE Computer Society Press.","DOI":"10.1109\/SFCS.1998.743523"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB29","unstructured":"J.C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using Muru. In Proc. IEEE Symp. Security and Privacy, pages 141\u2013151, 1997."},{"issue":"12","key":"10.1016\/S1571-0661(04)80968-X_NEWBIB30","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","article-title":"Using encryption for authentication in large networks of computers","volume":"21","author":"Needham","year":"1978","journal-title":"Communications of the ACM"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB31","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1109\/CSFW.1997.596790","article-title":"Mechanized proofs for a recursive authentication protocol","author":"Paulson","year":"1997","journal-title":"10th IEEE Computer Security Foundations Workshop"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB32","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1109\/CSFW.1997.596788","article-title":"Proving properties of security protocols by induction","author":"Paulson","year":"1997","journal-title":"10th IEEE Computer Security Foundations Workshop"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB33","doi-asserted-by":"crossref","unstructured":"B. Pfitzmann and M. Waidner. Composition and integrity preservation of secure reactive systems. In 7-th ACM Conference on Computer and Communications Security, Athens, November 2000, pages 245\u2013254. ACM Press, 2000. Preliminary version: IBM Research Report RZ 3234 (# 93280) 06\/12\/00, IBM Research Division, Z\u00fcrich, June 2000.","DOI":"10.1145\/352600.352639"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB34","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR. In CSFW VIII, page 98. IEEE Computer Soc Press, 1995.","DOI":"10.1109\/CSFW.1995.518556"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB35","article-title":"Security properties and CSP","author":"Schneider","year":"1996","journal-title":"IEEE Symp. Security and Privacy"},{"issue":"1","key":"10.1016\/S1571-0661(04)80968-X_NEWBIB36","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1006\/inco.1995.1123","article-title":"Reactive, generative and stratified models of probabilistic processes","volume":"121","author":"van Glabbeek","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80968-X_NEWBIB37","first-page":"80","article-title":"Theory and applications of trapdoor functions","author":"Yao","year":"1982","journal-title":"IEEE Foundations of Computer Science"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480968X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480968X?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:10:59Z","timestamp":1585897859000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610480968X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,11]]},"references-count":37,"alternative-id":["S157106610480968X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80968-x","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,11]]}}}