{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T01:43:49Z","timestamp":1775094229960,"version":"3.50.1"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319100814","type":"print"},{"value":"9783319100821","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10082-1_3","type":"book-chapter","created":{"date-parts":[[2014,8,4]],"date-time":"2014-08-04T04:49:05Z","timestamp":1407127745000},"page":"54-87","source":"Crossref","is-referenced-by-count":85,"title":["Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Blanchet","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Blanchet, B.: Secrecy types for asymmetric communication. Theoretical Computer Science\u00a0298(3), 387\u2013415 (2003), special issue FoSSaCS 2001","DOI":"10.1016\/S0304-3975(02)00863-0"},{"issue":"1","key":"3_CR2","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/1044731.1044735","volume":"52","author":"M. Abadi","year":"2005","unstructured":"Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. Journal of the ACM\u00a052(1), 102\u2013146 (2005)","journal-title":"Journal of the ACM"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Science of Computer Programming\u00a058(1-2), 3\u201327 (2005), special issue SAS 2003","DOI":"10.1016\/j.scico.2005.02.002"},{"issue":"3","key":"3_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1266977.1266978","volume":"10","author":"M. Abadi","year":"2007","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the pi calculus. ACM TISSEC\u00a010(3), 1\u201359 (2007)","journal-title":"ACM TISSEC"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001, pp. 104\u2013115. ACM Press, New York (2001)","DOI":"10.1145\/373243.360213"},{"key":"3_CR6","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1145\/511446.511497","volume-title":"11th International World Wide Web Conference","author":"M. Abadi","year":"2002","unstructured":"Abadi, M., Glew, N., Horne, B., Pinkas, B.: Certified email with a light on-line trusted third party: Design and implementation. In: 11th International World Wide Web Conference, pp. 387\u2013395. ACM, New York (2002)"},{"issue":"1","key":"3_CR7","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering\u00a022(1), 6\u201315 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"3_CR8","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1145\/996943.996946","volume":"7","author":"W. Aiello","year":"2004","unstructured":"Aiello, W., Bellovin, S.M., Blaze, M., Canetti, R., Ioannidis, J., Keromytis, K., Reingold, O.: Just Fast Keying: Key agreement in a hostile Internet. ACM TISSEC\u00a07(2), 242\u2013273 (2004)","journal-title":"ACM TISSEC"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Aizatulin, M., Gordon, A.D., J\u00fcrjens, J.: Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: CCS 2011, pp. 331\u2013340. ACM, New York (2011)","DOI":"10.1145\/2046707.2046745"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Allamigeon, X., Blanchet, B.: Reconstruction of attacks against cryptographic protocols. In: CSFW 2005, pp. 140\u2013154. IEEE, Los Alamitos (2005)","DOI":"10.1109\/CSFW.2005.25"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-540-77050-3_31","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"M. Arapinis","year":"2007","unstructured":"Arapinis, M., Duflot, M.: Bounding messages for free in security\u00a0protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855, pp. 376\u2013387. Springer, Heidelberg (2007)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., et al.: 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":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"875","DOI":"10.1007\/978-3-540-45236-2_47","volume-title":"FME 2003: Formal Methods","author":"A. Armando","year":"2003","unstructured":"Armando, A., Compagna, L., Ganty, P.: SAT-based model-checking of security protocols using planning graph analysis. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 875\u2013893. Springer, Heidelberg (2003)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, ch. 2, pp. 19\u2013100. North Holland (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: CSF 2008, pp. 195\u2013209. IEEE, Los Alamitos (2008)","DOI":"10.1109\/CSF.2008.26"},{"key":"3_CR16","unstructured":"Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: S& P 2008, pp. 202\u2013215. IEEE, Los Alamitos (2008), technical report version available at http:\/\/eprint.iacr.org\/2007\/289"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Bansal, C., Bhargavan, K., Maffeis, S.: Discovering concrete attacks on website authorization by formal analysis. In: CSF 2012, pp. 247\u2013262. IEEE, Los Alamitos (2012)","DOI":"10.1109\/CSF.2012.27"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G. Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol.\u00a06841, pp. 71\u201390. Springer, Heidelberg (2011)"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-39650-5_15","volume-title":"Computer Security \u2013 ESORICS 2003","author":"D. Basin","year":"2003","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: An on-the-fly model-checker for security protocol analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol.\u00a02808, pp. 253\u2013270. Springer, Heidelberg (2003)"},{"key":"3_CR20","first-page":"459","volume-title":"CCS 2008","author":"K. Bhargavan","year":"2008","unstructured":"Bhargavan, K., Corin, R., Fournet, C., Z\u0103linescu, E.: Cryptographically verified implementations for TLS. In: CCS 2008, pp. 459\u2013468. ACM, New York (2008)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.: Verifying policy-based security for web services. In: CCS 2004, pp. 268\u2013277. ACM, New York (2004)","DOI":"10.1145\/1111348.1111355"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Gordon, A., Tse, S.: Verified interoperable implementations of security protocols. In: CSFW 2006, pp. 139\u2013152. IEEE, Los Alamitos (2006)","DOI":"10.1007\/11841197_6"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW-14, pp. 82\u201396. IEEE, Los Alamitos (June 2001)","DOI":"10.1109\/CSFW.2001.930138"},{"issue":"5","key":"3_CR24","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.ipl.2005.05.011","volume":"95","author":"B. Blanchet","year":"2005","unstructured":"Blanchet, B.: Security protocols: From linear to classical logic by abstract interpretation. Information Processing Letters\u00a095(5), 473\u2013479 (2005)","journal-title":"Information Processing Letters"},{"key":"3_CR25","unstructured":"Blanchet, B.: Automatic verification of correspondences for security protocols. Report arXiv:0802.3444v1 (2008), http:\/\/arxiv.org\/abs\/0802.3444v1"},{"issue":"4","key":"3_CR26","doi-asserted-by":"publisher","first-page":"363","DOI":"10.3233\/JCS-2009-0339","volume":"17","author":"B. Blanchet","year":"2009","unstructured":"Blanchet, B.: Automatic verification of correspondences for security protocols. Journal of Computer Security\u00a017(4), 363\u2013434 (2009)","journal-title":"Journal of Computer Security"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Mechanizing game-based proofs of security protocols. In: Nipkow, T., Grumberg, O., Hauptmann, B. (eds.) Software Safety and Security - Tools for Analysis and Verification. NATO Science for Peace and Security Series \u2013 D: Information and Communication Security, vol.\u00a033, pp. 1\u201325. IOS Press (May 2012), Proceedings of the 2011 MOD Summer School","DOI":"10.3233\/978-1-61499-028-4-1"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-28641-4_2","volume-title":"Principles of Security and Trust","author":"B. Blanchet","year":"2012","unstructured":"Blanchet, B.: Security protocol verification: Symbolic and computational models. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol.\u00a07215, pp. 3\u201329. Springer, Heidelberg (2012)"},{"issue":"1","key":"3_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2007.06.002","volume":"75","author":"B. Blanchet","year":"2008","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming\u00a075(1), 3\u201351 (2008)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Chaudhuri, A.: Automated formal analysis of a protocol for secure file sharing on untrusted storage. In: S&P 2008, pp. 417\u2013431. IEEE, Los Alamitos (2008)","DOI":"10.1109\/SP.2008.12"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. Theoretical Computer Science\u00a0333(1-2), 67\u201390 (2005), special issue FoSSaCS 2003","DOI":"10.1016\/j.tcs.2004.10.018"},{"key":"3_CR32","unstructured":"Bodei, C.: Security Issues in Process Calculi. Ph.D. thesis, Universit\u00e0 di Pisa (January 2000)"},{"key":"3_CR33","unstructured":"Boichut, Y., Kosmatov, N., Vigneron, L.: Validation of Prouv\u00e9 protocols using the automatic tool TA4SP. In: Proceedings of the Third Taiwanese-French Conference on Information Technology (TFIT 2006), Nancy, France, pp. 467\u2013480 (March 2006)"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/11681878_20","volume-title":"Theory of Cryptography","author":"R. Canetti","year":"2006","unstructured":"Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol.\u00a03876, pp. 380\u2013403. Springer, Heidelberg (2006), extended version available at http:\/\/eprint.iacr.org\/2004\/334"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-44618-4_27","volume-title":"CONCUR 2000 - Concurrency Theory","author":"L. Cardelli","year":"2000","unstructured":"Cardelli, L., Ghelli, G., Gordon, A.D.: Secrecy and group creation. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 365\u2013379. Springer, Heidelberg (2000)"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-24597-1_11","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"Y. Chevalier","year":"2003","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 124\u2013135. Springer, Heidelberg (2003)"},{"issue":"1-3","key":"3_CR37","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/j.tcs.2005.01.015","volume":"338","author":"Y. Chevalier","year":"2005","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. Theoretical Computer Science\u00a0338(1-3), 247\u2013274 (2005)","journal-title":"Theoretical Computer Science"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Vigneron, L.: A tool for lazy verification of security protocols. In: ASE 2001, pp. 373\u2013376. IEEE, Los Alamitos (2001)","DOI":"10.1109\/ASE.2001.989832"},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-44881-0_12","volume-title":"Rewriting Techniques and Applications","author":"H. Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 148\u2013164. Springer, Heidelberg (2003)"},{"issue":"1-3","key":"3_CR40","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.scico.2003.12.002","volume":"50","author":"H. Comon-Lundh","year":"2004","unstructured":"Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. Science of Computer Programming\u00a050(1-3), 51\u201371 (2004)","journal-title":"Science of Computer Programming"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: LICS 2003, pp. 271\u2013280. IEEE, Los Alamitos (2003)","DOI":"10.1109\/LICS.2003.1210067"},{"key":"3_CR42","unstructured":"Cremers, C.J.F.: Scyther - Semantics and Verification of Security Protocols. Ph.D. dissertation, Eindhoven University of Technology (2006)"},{"key":"3_CR43","unstructured":"Denker, G., Meseguer, J., Talcott, C.: Protocol specification and analysis in Maude. In: FMSP 1998 (June 1998)"},{"issue":"8","key":"3_CR44","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"D.E. Denning","year":"1981","unstructured":"Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Commun. ACM\u00a024(8), 533\u2013536 (1981)","journal-title":"Commun. ACM"},{"issue":"6","key":"3_CR45","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"IT-22","author":"W. Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.: New directions in cryptography. IEEE Transactions on Information Theory\u00a0IT-22(6), 644\u2013654 (1976)","journal-title":"IEEE Transactions on Information Theory"},{"issue":"12","key":"3_CR46","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"IT-29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory\u00a0IT-29(12), 198\u2013208 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"issue":"2","key":"3_CR47","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-2004-12203","volume":"12","author":"N. Durgin","year":"2004","unstructured":"Durgin, N., Lincoln, P., Mitchell, J.C., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security\u00a012(2), 247\u2013311 (2004)","journal-title":"Journal of Computer Security"},{"issue":"1-2","key":"3_CR48","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S. Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theoretical Computer Science\u00a0367(1-2), 162\u2013202 (2006)","journal-title":"Theoretical Computer Science"},{"key":"3_CR49","unstructured":"Godskesen, J.C.: Formal verification of the ARAN protocol using the applied pi-calculus. In: WITS 2006, pp. 99\u2013113 (March 2006)"},{"issue":"3\/4","key":"3_CR50","doi-asserted-by":"publisher","first-page":"435","DOI":"10.3233\/JCS-2004-123-406","volume":"12","author":"A. Gordon","year":"2004","unstructured":"Gordon, A., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. Journal of Computer Security\u00a012(3\/4), 435\u2013484 (2004)","journal-title":"Journal of Computer Security"},{"issue":"3","key":"3_CR51","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1016\/j.ipl.2005.04.007","volume":"95","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J.: Deciding ${\\cal H}_1$ by resolution. Information Processing Letters\u00a095(3), 401\u2013408 (2005)","journal-title":"Information Processing Letters"},{"key":"3_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-30579-8_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 363\u2013379. Springer, Heidelberg (2005)"},{"key":"3_CR53","doi-asserted-by":"crossref","unstructured":"Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: CSFW 2000, pp. 255\u2013268. IEEE, Los Alamitos (2000)","DOI":"10.1109\/CSFW.2000.856942"},{"key":"3_CR54","unstructured":"Kallahalla, M., Riedel, E., Swaminathan, R., Wang, Q., Fu, K.: Plutus: Scalable secure file sharing on untrusted storage. In: FAST 2003, pp. 29\u201342. Usenix, Berkeley (2003)"},{"key":"3_CR55","first-page":"46","volume-title":"ASIACCS 2006","author":"H. Khurana","year":"2006","unstructured":"Khurana, H., Hahm, H.S.: Certified mailing lists. In: ASIACCS 2006, pp. 46\u201358. ACM, New York (2006)"},{"key":"3_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-540-31987-0_14","volume-title":"Programming Languages and Systems","author":"S. Kremer","year":"2005","unstructured":"Kremer, S., Ryan, M.D.: Analysis of an electronic voting protocol in the applied pi calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 186\u2013200. Springer, Heidelberg (2005)"},{"key":"3_CR57","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach. In: CCS 2008, pp. 129\u2013138. ACM, New York (2008)","DOI":"10.1145\/1455770.1455788"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: CSF 2009, pp. 157\u2013171. IEEE, Los Alamitos (2009)","DOI":"10.1109\/CSF.2009.17"},{"key":"3_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"3_CR60","doi-asserted-by":"crossref","unstructured":"Lux, K.D., May, M.J., Bhattad, N.L., Gunter, C.A.: WSEmail: Secure internet messaging based on web services. In: ICWS 2005, pp. 75\u201382. IEEE, Los Alamitos (2005)","DOI":"10.1109\/ICWS.2005.138"},{"issue":"1","key":"3_CR61","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1006\/jsco.1996.0075","volume":"21","author":"C. Lynch","year":"1997","unstructured":"Lynch, C.: Oriented equational logic programming is complete. Journal of Symbolic Computation\u00a021(1), 23\u201345 (1997)","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"3_CR62","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C.A. Meadows","year":"1996","unstructured":"Meadows, C.A.: The NRL protocol analyzer: An overview. Journal of Logic Programming\u00a026(2), 113\u2013131 (1996)","journal-title":"Journal of Logic Programming"},{"key":"3_CR63","unstructured":"Meadows, C., Narendran, P.: A unification algorithm for the group Diffie-Hellman protocol. In: WITS 2002 (January 2002)"},{"issue":"2-3","key":"3_CR64","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0167-6423(02)00132-6","volume":"47","author":"D. Monniaux","year":"2003","unstructured":"Monniaux, D.: Abstracting cryptographic protocols with tree automata. Science of Computer Programming\u00a047(2-3), 177\u2013202 (2003)","journal-title":"Science of Computer Programming"},{"issue":"12","key":"3_CR65","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM\u00a021(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"key":"3_CR66","unstructured":"de Nivelle, H.: Ordering Refinements of Resolution. Ph.D. thesis, Technische Universiteit Delft (October 1995)"},{"issue":"1-2","key":"3_CR67","doi-asserted-by":"publisher","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":"3_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-24597-1_31","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"R. Ramanujam","year":"2003","unstructured":"Ramanujam, R., Suresh, S.P.: Tagging makes secrecy decidable with unbounded nonces as well. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 363\u2013374. Springer, Heidelberg (2003)"},{"issue":"1-3","key":"3_CR69","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1016\/S0304-3975(02)00490-5","volume":"299","author":"M. Rusinowitch","year":"2003","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. Theoretical Computer Science\u00a0299(1-3), 451\u2013475 (2003)","journal-title":"Theoretical Computer Science"},{"key":"3_CR70","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: CSF 2012, pp. 78\u201394. IEEE, Los Alamitos (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"3_CR71","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE-16. LNCS (LNAI), vol.\u00a01632, pp. 314\u2013328. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security Analysis and Design VII"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10082-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T01:54:25Z","timestamp":1746323665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10082-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319100814","9783319100821"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10082-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}