{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:32:14Z","timestamp":1742380334007},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2004,4,6]],"date-time":"2004-04-06T00:00:00Z","timestamp":1081209600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2004,7]]},"DOI":"10.1007\/s10009-003-0136-3","type":"journal-article","created":{"date-parts":[[2004,4,7]],"date-time":"2004-04-07T08:17:12Z","timestamp":1081325832000},"page":"38-66","source":"Crossref","is-referenced-by-count":15,"title":["A logical encoding of the \u03c0-calculus: model checking mobile processes using tabled resolution"],"prefix":"10.1007","volume":"6","author":[{"given":"Ping","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.R.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,4,6]]},"reference":[{"key":"136_CR1","doi-asserted-by":"crossref","unstructured":"Abadi M, Blanchet B (2002) Analyzing security protocols with secrecy types and logic programs. In: Proceedings of the 29th annual ACM SIGPLAN \u2013 SIGACT symposium on principles of programming languages (POPL 2002), Portland, OR, January 2002. ACM Press, New York, pp 33\u201344","DOI":"10.1145\/565816.503277"},{"key":"136_CR2","doi-asserted-by":"crossref","unstructured":"Abadi M, Gordon AD (1997) A calculus for cryptographic protocols: the spi calculus. In: Proceedings of the 4th ACM conference on computer and communications security, Zurich, Switzerland, April 1997. ACM Press, New York, pp 36\u201347","DOI":"10.1145\/266420.266432"},{"key":"136_CR3","first-page":"267","volume":"5","author":"Abadi","year":"1998","unstructured":"Abadi M, Gordon AD (1998) A bisimulation method for cryptographic protocols. Nordic J Comput 5(4):267\u2013303","journal-title":"Nordic J Comput"},{"key":"136_CR4","doi-asserted-by":"crossref","unstructured":"Apt K (1990) Logic programming. In: Van Leeuwen J (ed) Handbook of theoretical computer science, vol B: Formal models and semantics. Elsevier\/MIT Press, Amsterdam\/Cambridge, MA, pp 493\u2013574","DOI":"10.1016\/B978-0-444-88074-1.50015-9"},{"key":"136_CR5","unstructured":"Aziz B, Hamilton GW (2002) A privacy analysis for the pi-calculus: the denotational approach. In: Proceedings of the 2nd workshop on the specification, analysis and validation for emerging technologies, Copenhagen, July 2002"},{"key":"136_CR6","doi-asserted-by":"crossref","unstructured":"Basu S, Mukund M, Ramakrishnan CR, Ramakrishnan IV, Verma RM (2001) Local and symbolic bisimulation using tabled constraint logic programming. In: Proceedings of the international conference on logic programming, Cyprus, November 2001, pp 166\u2013180","DOI":"10.1007\/3-540-45635-X_19"},{"key":"136_CR7","unstructured":"Beste FB (1998) The model prover \u2013 a sequent-calculus based modal \u03bc-calculus model checker tool for finite control \u03c0-calculus agents. Technical report, Swedish Institute of Computer Science, Kista, Sweden"},{"key":"136_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet B (2002) From secrecy to authenticity in security protocols. In: Hermenegildo M, Puebla G (eds) Proceedings of the 9th international static analysis symposium, Madrid, September 2002. Lecture notes in computer science, vol 2477. Springer, Berlin Heidelberg New York, pp 242\u2013259","DOI":"10.1007\/3-540-45789-5_25"},{"key":"136_CR9","doi-asserted-by":"crossref","unstructured":"Blanchet B, Podelski A (2003) Verification of cryptographic protocols: tagging enforces termination. In: Proceedings of the conference on foundations of software science and computation structures (FoSSaCS\u201903), Warsaw, Poland, April 2003. Lecture notes in computer science, vol 2620. Springer, Berlin Heidelberg New York, pp 136\u2013152","DOI":"10.1007\/3-540-36576-1_9"},{"key":"136_CR10","doi-asserted-by":"crossref","unstructured":"Burrows M, Abadi M, Needham R (1996) A logic of authentication, from Proceedings of the Royal Society 426(1871), 1989. In: Stallings W (ed) Practical cryptography for data Internetworks. IEEE Press, New York","DOI":"10.1098\/rspa.1989.0125"},{"key":"136_CR11","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/227595.227597","volume":"43","author":"Chen","year":"1996","unstructured":"Chen W, Warren DS (1996) Tabled evaluation with delaying for general logic programs. J ACM 43(1):20\u201374","journal-title":"J ACM"},{"key":"136_CR12","unstructured":"Cohen E (2002) Proving protocols safe from guessing. In: Proceedings of the workshop on foundations of computer security (FCS\u201902), Copenhagen, July 2002, pp 85\u201392"},{"key":"136_CR13","doi-asserted-by":"crossref","unstructured":"Cui B, Warren DS (2000) A system for tabled constraint logic programming. In: Proceedings of the 1st international conference on computational logic, London, UK, July 2000. Lecture notes in computer science, vol 1861. Springer, Berlin Heidelberg New York, pp 478\u2013492","DOI":"10.1007\/3-540-44957-4_32"},{"key":"136_CR14","unstructured":"Dam M (2001) Proof systems for pi-calculus logics. Logic for concurrency and synchronisation, Kluwer, Dordrecht, pp 145\u2013212"},{"key":"136_CR15","unstructured":"Denker G, Meseguer J (1998) Protocol specification and analysis in Maude. In: Proceedings of the workshop on formal methods and security protocols, Indianapolis, IN, June 1998"},{"key":"136_CR16","doi-asserted-by":"crossref","unstructured":"Dong Y, Ramakrishnan CR (1999) An optimizing compiler for efficient model checking. In: Formal methods for protocol engineering and distributed systems (FORTE). Proceedings of IFIP, Beijing, October 1999. Kluwer, Dordrecht, 156:241\u2013256","DOI":"10.1007\/978-0-387-35578-8_14"},{"key":"136_CR17","doi-asserted-by":"crossref","unstructured":"Duran F, Eker S, Lincoln P, Meseguer J (2000) Principles of mobile Maude. In: Kotz D, Mattern F (eds) Proceedings of ASA\/MA, Switzerland, September 2000. Lecture notes in computer science, vol 1882. Springer, Berlin Heidelberg New York, pp 73\u201385","DOI":"10.1007\/978-3-540-45347-5_7"},{"key":"136_CR18","unstructured":"Franzen T (1996) A theorem-proving approach to deciding properties of finite-control agents. Technical report, Swedish Institute of Computer Science, Kista, Sweden"},{"key":"136_CR19","doi-asserted-by":"crossref","unstructured":"Gordon A, Jeffrey ASA (2001) Authenticity by typing for security protocols. In: Proceedings of the IEEE computer security foundations workshop, Cape Breton, Novia Scotia, Canada, June 2001, pp 145\u2013159","DOI":"10.1109\/CSFW.2001.930143"},{"key":"136_CR20","doi-asserted-by":"crossref","unstructured":"H\u00fcttel H (2002) Deciding framed bisimilarity. In: Proceedings of the 4th international workshop on verification of infinite-state systems (INFINITY 2002), Brno, Czech Republic, August 2002","DOI":"10.7146\/brics.v9i25.21741"},{"key":"136_CR21","unstructured":"Lin H (1994) Symbolic bisimulation and proof systems for the \u03c0-calculus. Technical report, School of Cognitive and Computer Science, University of Sussex, Sussex, UK"},{"key":"136_CR22","doi-asserted-by":"crossref","unstructured":"Lloyd JW (1984) Foundations of logic programming. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-3-642-96826-6"},{"key":"136_CR23","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"Lowe","year":"1995","unstructured":"Lowe G (1995) An attack on the Needham\u2013Schroeder public-key authentication protocol. Inf Process Lett 56(3):131\u2013133","journal-title":"Inf Process Lett"},{"key":"136_CR24","first-page":"93","volume":"17","author":"Lowe","year":"1996","unstructured":"Lowe G (1996) Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Softw Concepts Tools 17:93\u2013102","journal-title":"Softw Concepts Tools"},{"key":"136_CR25","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"Meadows","year":"1996","unstructured":"Meadows C (1996) The NRL protocol analyzer: an overview. J Logic Programm 26(2):113\u2013131","journal-title":"J Logic Programm"},{"key":"136_CR26","doi-asserted-by":"crossref","unstructured":"Millen J, Shmatikov V (2001) Constraint solving for bounded process cryptographic protocol analysis. In: Proceedings of the 8th ACM conference on computer and communications security, Philadelphia, November 2001. ACM Press, New York","DOI":"10.1145\/501983.502007"},{"key":"136_CR27","unstructured":"Milner R (1989) Communication and concurrency. In: International Series in Computer Science. Prentice-Hall, Upper Saddle River, NJ"},{"key":"136_CR28","doi-asserted-by":"crossref","unstructured":"Milner R (1993) The polyadic \u03c0-calculus: a tutorial. In: Bauer FL, Brauer W, Schwichtenberg H (eds) Logic and algebra of specification. Springer, Berlin Heidelberg New York, pp 203\u2013246","DOI":"10.1007\/978-3-642-58041-3_6"},{"key":"136_CR29","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"Milner","year":"1992","unstructured":"Milner R, Parrow J, Walker D (1992) A calculus of mobile processes, parts I and II. Inf Comput 100(1):1\u201377","journal-title":"Inf Comput"},{"key":"136_CR30","doi-asserted-by":"crossref","unstructured":"Milner R, Parrow J, Walker D (1993) Modal logics for mobile processes. Theor Comput Sci pp 149\u2013171","DOI":"10.1016\/0304-3975(93)90156-N"},{"key":"136_CR31","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/BF01211473","volume":"4","author":"Orava","year":"1992","unstructured":"Orava F, Parrow J (1992) An algebraic verification of a mobile network. Formal Aspects Comput 4:497\u2013543","journal-title":"Formal Aspects Comput"},{"key":"136_CR32","doi-asserted-by":"crossref","unstructured":"Parrow J (2001) An introduction to the \u03c0-calculus. In: Bergstra JA, Ponse A, Smolka SA (eds) Handbook of process algebra. Elsevier, Amsterdam","DOI":"10.1016\/B978-044482830-9\/50026-6"},{"key":"136_CR33","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"Paulson","year":"1998","unstructured":"Paulson L (1998) The inductive approach to verifying cryptographic protocols. J Comput Secur 6:85\u2013128","journal-title":"J Comput Secur"},{"key":"136_CR34","doi-asserted-by":"crossref","unstructured":"Ramakrishna YS, Ramakrishnan CR, Ramakrishnan IV, Smolka SA, Swift TW, Warren DS (1997) Efficient model checking using tabled resolution. In: Proceedings of the 9th international conference on computer-aided verification (CAV), Haifa, Israel, June 1997. Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 143\u2013154","DOI":"10.1007\/3-540-63166-6_16"},{"key":"136_CR35","doi-asserted-by":"crossref","unstructured":"Roychoudhury A, Narayan Kumar K, Ramakrishnan CR, Ramakrishnan IV, Smolka SA (2000) Verification of parameterized systems using logic-program transformations. In: Proceedings of the 6th international conference on tools and algorithms for the construction and analysis of systems (TACAS), Berlin, March 2000. Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 172\u2013187","DOI":"10.1007\/3-540-46419-0_13"},{"key":"136_CR36","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"Stirling","year":"1991","unstructured":"Stirling C, Walker D (1991) Local model checking in the modal mu-calculus. Theor Comput Sci 89(1):161\u2013177","journal-title":"Theor Comput Sci"},{"key":"136_CR37","doi-asserted-by":"crossref","unstructured":"Syverson P (1994) A taxonomy of replay attacks. In: Proceedings of the computer security foundations workshop VII, Franconia, NH, June 1994. IEEE Press, New York","DOI":"10.1109\/CSFW.1994.315935"},{"key":"136_CR38","doi-asserted-by":"crossref","unstructured":"Tamaki H, Sato T (1986) OLDT resolution with tabulation. In: Proceedings of the international conference on logic programming, London, UK, July 1986. MIT Press, Cambridge, MA, pp 84\u201398","DOI":"10.1007\/3-540-16492-8_66"},{"key":"136_CR39","unstructured":"Thati P, Sen K, Marti-oliet N (2002) An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0. In: Proceedings of the 4th international workshop on rewriting logic and its applications, Italy, September 2002"},{"key":"136_CR40","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"Thayer","year":"1999","unstructured":"Thayer Fabrega FJ, Herzog JC, Guttman JD (1999) Strand spaces: proving security protocol correct. J Comput Secur 7:191\u2013230","journal-title":"J Comput Secur"},{"key":"136_CR41","unstructured":"Victor B (1995) The Mobility Workbench user\u2019s guide. Technical report, Department of Computer Systems, Uppsala University, Sweden"},{"key":"136_CR42","doi-asserted-by":"crossref","unstructured":"Victor B, Moller F (1994) The Mobility Workbench \u2013 a tool for the \u03c0-calculus. In: Dill D (ed) Proceedings of the 6th international conference on computer-aided verification (CAV \u201994), Stanford, CA, June 1994. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-58179-0_73"},{"key":"136_CR43","doi-asserted-by":"crossref","unstructured":"Woo TYC, Lam SS (1993) A semantic model for authentication protocols. In: Proceedings of the IEEE symposium on research in security and privacy, Oakland, CA, May 1993, pp 178\u2013194","DOI":"10.1109\/RISP.1993.287633"},{"key":"136_CR44","unstructured":"XSB The XSB logic programming system. http:\/\/xsb.sourceforge.net"},{"key":"136_CR45","unstructured":"Yang P, Ramakrishnan CR, Smolka SA (2002) Mobility Model Checker for the \u03c0-calculus. http:\/\/www.cs.sunysb.edu\/\u223clmc\/mmc"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0136-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0136-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0136-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:18Z","timestamp":1559114718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0136-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4,6]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["136"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0136-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4,6]]}}}