{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:37Z","timestamp":1760202577282},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540694052"},{"type":"electronic","value":"9783540694076"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69407-6_33","type":"book-chapter","created":{"date-parts":[[2008,6,10]],"date-time":"2008-06-10T13:39:35Z","timestamp":1213105175000},"page":"294-305","source":"Crossref","is-referenced-by-count":4,"title":["Implementing Spi Calculus Using Nominal Techniques"],"prefix":"10.1007","author":[{"given":"Temesghen","family":"Kahsai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marino","family":"Miculan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"33_CR1","first-page":"267","volume":"5","author":"M. Abadi","year":"1998","unstructured":"Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. Nord. J. Comput.\u00a05(4), 267 (1998)","journal-title":"Nord. J. Comput."},{"issue":"1","key":"33_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The Spi calculus. Journal of Information and Computation\u00a0148(1), 1\u201370 (1999)","journal-title":"Journal of Information and Computation"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., Basin, D.A., Boichut, Y., Chevalier, Y., Compagna, L., Cu\u00e9llar, J., Drielsma, P.H., H\u00e9am, P.-C., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-71389-0_6","volume-title":"Foundations of Software Science and Computational Structures","author":"J. Bengtson","year":"2007","unstructured":"Bengtson, J., Parrow, J.: Formalising the \u03c0-calculus using nominal logic. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, pp. 63\u201377. Springer, Heidelberg (2007)"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45789-5_25","volume-title":"Static Analysis","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B.: From secrecy to authenticity in security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 342\u2013359. Springer, Heidelberg (2002)"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Proc.\u00a020th LICS, pp. 331\u2013340. IEEE (2005)","DOI":"10.1109\/LICS.2005.8"},{"issue":"3","key":"33_CR7","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1137\/S0097539700377864","volume":"31","author":"M. Boreale","year":"2001","unstructured":"Boreale, M., Nicola, R.D., Pugliese, R.: Proof techniques for cryptographic processes. SIAM J. Comput.\u00a031(3), 947\u2013986 (2001)","journal-title":"SIAM J. Comput."},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-540-28644-8_11","volume-title":"CONCUR 2004 - Concurrency Theory","author":"J. Borgstr\u00f6m","year":"2004","unstructured":"Borgstr\u00f6m, J., Briais, S., Nestmann, U.: Symbolic bisimulation in the spi calculus. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 161\u2013176. Springer, Heidelberg (2004)"},{"issue":"3","key":"33_CR9","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1017\/S0960129505004706","volume":"15","author":"J. Borgstr\u00f6m","year":"2005","unstructured":"Borgstr\u00f6m, J., Nestmann, U.: On bisimulations for the spi calculus. Mathematical Structures in Computer Science\u00a015(3), 487\u2013552 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"4","key":"33_CR10","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1145\/363516.363528","volume":"9","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Jha, S., Marrero, W.: Verifying security protocols with brutus. ACM Trans. Softw. Eng. Methodol.\u00a09(4), 443\u2013487 (2000)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax involving binders. In: Proc. 14th LICS, pp. 214\u2013224. IEEE (1999)","DOI":"10.1109\/LICS.1999.782617"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028392","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Hirschkoff","year":"1997","unstructured":"Hirschkoff, D.: Bisimulation proofs for the \u03c0-calculus in the Calculus of Constructions. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275. Springer, Heidelberg (1997)"},{"issue":"2","key":"33_CR13","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F. Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: \u03c0-calculus in (co)inductive type theory. Theoretical Computer Science\u00a0253(2), 239\u2013285 (2001)","journal-title":"Theoretical Computer Science"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"H\u00fcttel, H.: Deciding framed bisimilarity. In: Proceedings of Infinity 2002. Electronic Notes in Theoretical Computer Science, vol.\u00a068, pp. 1\u201318 (2003)","DOI":"10.1016\/S1571-0661(04)80530-9"},{"issue":"1","key":"33_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Inform.\u00a0and\u00a0Comput.\u00a0100(1), 1\u201377 (1992)","journal-title":"Inform.\u00a0and\u00a0Comput."},{"key":"33_CR16","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Mur\u03c6. In: IEEE Symposium on Security and Privacy, pp. 141\u2013151. IEEE Computer Society (1997)","DOI":"10.1109\/SECPRI.1997.601329"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 2\u201313. Springer, Heidelberg (2001)"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"673","DOI":"10.1007\/3-540-55602-8_201","volume-title":"Automated Deduction - CADE-11","author":"T. Nipkow","year":"1992","unstructured":"Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 673\u2013676. Springer, Heidelberg (1992)"},{"issue":"1-2","key":"33_CR19","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security\u00a06(1-2), 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"33_CR20","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation\u00a0186, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: Proc.\u00a0LICS, pp. 293\u2013302. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.17"},{"key":"33_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/11532231_4","volume-title":"Automated Deduction \u2013 CADE-20","author":"C. Urban","year":"2005","unstructured":"Urban, C., Tasson, C.: Nominal techniques in Isabelle\/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 38\u201353. Springer, Heidelberg (2005)"},{"key":"33_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013184. Springer, Heidelberg (1999)"},{"key":"33_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"442","DOI":"10.1007\/3-540-63533-5_23","volume-title":"FME \u201997 Industrial Applications and Strengthened Foundations of Formal Methods","author":"S. Yu","year":"1997","unstructured":"Yu, S., Luo, Z.: Implementing a model checker for LEGO. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol.\u00a01313, pp. 442\u2013458. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Logic and Theory of Algorithms"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69407-6_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:38:32Z","timestamp":1620016712000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69407-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540694052","9783540694076"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69407-6_33","relation":{},"subject":[]}}