{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T17:38:30Z","timestamp":1748367510641},"publisher-location":"Berlin, Heidelberg","reference-count":83,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540748090"},{"type":"electronic","value":"9783540748106"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74810-6_1","type":"book-chapter","created":{"date-parts":[[2007,8,17]],"date-time":"2007-08-17T01:44:24Z","timestamp":1187315064000},"page":"1-23","source":"Crossref","is-referenced-by-count":8,"title":["Security Protocols: Principles and Calculi"],"prefix":"10.1007","author":[{"given":"Mart\u00edn","family":"Abadi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"unstructured":"Abadi, M.: Security protocols: Principles and calculi. Lectures at 6th International School on Foundations of Security Analysis and Design (September 2006), Slides at http:\/\/www.sti.uniurb.it\/events\/fosad06\/papers\/Abadi-fosad06.pdf","key":"1_CR1"},{"issue":"1","key":"1_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"},{"issue":"1-2","key":"1_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2005.02.002","volume":"58","author":"M. Abadi","year":"2005","unstructured":"Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Science of Computer Programming\u00a058(1-2), 3\u201327 (2005)","journal-title":"Science of Computer Programming"},{"doi-asserted-by":"crossref","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the pi calculus. ACM Transactions on Information and System Security (to appear, 2007)","key":"1_CR4","DOI":"10.1145\/1266977.1266978"},{"issue":"1-2","key":"1_CR5","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"367","author":"M. Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science\u00a0367(1-2), 2\u201332 (2006)","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104\u2013115 (January 2001)","key":"1_CR6","DOI":"10.1145\/360204.360213"},{"issue":"3","key":"1_CR7","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1016\/j.tcs.2003.12.023","volume":"322","author":"M. Abadi","year":"2004","unstructured":"Abadi, M., Fournet, C.: Private authentication. Theoretical Computer Science\u00a0322(3), 427\u2013476 (2004)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1998","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus (An extended version appeared as Digital Equipment Corporation Systems Research Center report No. 149, January 1998). Information and Computation\u00a0148(1), 1\u201370 (1998)","journal-title":"Information and Computation"},{"issue":"1","key":"1_CR9","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":"1_CR10","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s00145-001-0014-7","volume":"15","author":"M. Abadi","year":"2002","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). Journal of Cryptology\u00a015(2), 103\u2013127 (2002)","journal-title":"Journal of Cryptology"},{"issue":"2","key":"1_CR11","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, A.D., Reingold, O.: Just Fast Keying: Key agreement in a hostile internet. ACM Transactions on Information and System Security\u00a07(2), 242\u2013273 (2004)","journal-title":"ACM Transactions on Information and System Security"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-44618-4_28","volume-title":"CONCUR 2000 - Concurrency Theory","author":"R. Amadio","year":"2000","unstructured":"Amadio, R., Lugiez, D.: On the reachability problem in cryptographic protocols. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 380\u2013395. Springer, Heidelberg (2000)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/3-540-46674-6_3","volume-title":"Advances in Computing Science - ASIAN\u201999","author":"R. Amadio","year":"1999","unstructured":"Amadio, R., Prasad, S.: The game of the name in cryptographic tables. In: Thiagarajan, P.S., Yap, R.H.C. (eds.) ASIAN 1999. LNCS, vol.\u00a01742, pp. 15\u201327. Springer, Heidelberg (1999)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/3-540-44750-4_19","volume-title":"Advances in Cryptology - CRYPTO \u201995","author":"R. Anderson","year":"1995","unstructured":"Anderson, R., Needham, R.: Robustness principles for public key protocols. In: Coppersmith, D. (ed.) CRYPTO 1995. LNCS, vol.\u00a0963, pp. 236\u2013247. Springer, Heidelberg (1995)"},{"doi-asserted-by":"crossref","unstructured":"Aura, T.: Strategies against replay attacks. In: 10th IEEE Computer Security Foundations Workshop, pp. 59\u201368 (1997)","key":"1_CR15","DOI":"10.1109\/CSFW.1997.596787"},{"doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: 10th ACM conference on Computer and Communications security (CCS 2003), pp. 220\u2013230 (October 2003)","key":"1_CR16","DOI":"10.1145\/948109.948140"},{"doi-asserted-by":"crossref","unstructured":"Baldamus, M., Parrow, J., Victor, B.: Spi calculus translated to pi-calculus preserving may-tests. In: 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 22\u201331 (July 2004)","key":"1_CR17","DOI":"10.1109\/LICS.2004.1319597"},{"unstructured":"Baudet, M.: S\u00e9curit\u00e9 des protocoles cryptographiques: aspects logiques et calculatoires. PhD thesis, Ecole Normale Sup\u00e9rieure de Cachan (2007)","key":"1_CR18"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-48329-2_21","volume-title":"Advances in Cryptology - CRYPTO \u201993","author":"M. Bellare","year":"1994","unstructured":"Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol.\u00a0773, pp. 232\u2013249. Springer, Heidelberg (1994)"},{"doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D.: Verifying policy-based security for web services. In: ACM Conference on Computer and Communications Security (CCS 2004), pp. 268\u2013277 (October 2004)","key":"1_CR20","DOI":"10.1145\/1030083.1030120"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/11841197_6","volume-title":"Web Services and Formal Methods","author":"K. Bhargavan","year":"2006","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D.: Verified reference implementations of WS-security protocols. In: Bravetti, M., N\u00fa\u00f1ez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol.\u00a04184, pp. 88\u2013106. Springer, Heidelberg (2006)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-540-30101-1_9","volume-title":"Formal Methods for Components and Objects","author":"K. Bhargavan","year":"2004","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D., Pucella, R.: TulaFale: A security tool for web services. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol.\u00a03188, pp. 197\u2013222. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82\u201396 (June 2001)","key":"1_CR23","DOI":"10.1109\/CSFW.2001.930138"},{"key":"1_CR24","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)"},{"doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: 2004 IEEE Symposium on Security and Privacy, pp. 86\u2013100 (May 2004)","key":"1_CR25","DOI":"10.1109\/SECPRI.2004.1301317"},{"doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: 2006 IEEE Symposium on Security and Privacy, pp. 140\u2013154 (May 2006)","key":"1_CR26","DOI":"10.1109\/SP.2006.1"},{"doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming (to appear, 2007)","key":"1_CR27","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/3-540-36576-1_9","volume-title":"Foundations of Software Science and Computation Structures: 6th International Conference, FOSSACS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. In: Gordon, A.D. (ed.) ETAPS 2003 and FOSSACS 2003. LNCS, vol.\u00a02620, pp. 136\u2013152. Springer, Heidelberg (2003)"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/11818175_32","volume-title":"Advances in Cryptology - CRYPTO 2006","author":"B. Blanchet","year":"2006","unstructured":"Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol.\u00a04117, pp. 537\u2013554. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Blum, M., Micali, S.: How to generate cryptographically strong sequences of pseudo random bits. In: 23rd Annual Symposium on Foundations of Computer Science (FOCS 1982), pp. 112\u2013117 (1982)","key":"1_CR30","DOI":"10.1109\/SFCS.1982.72"},{"issue":"6","key":"1_CR31","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1016\/S0167-739X(02)00047-X","volume":"18","author":"C. Bodei","year":"2002","unstructured":"Bodei, C., Degano, P., Nielson, F., Nielson, H.: Flow logic for Dolev-Yao secrecy in cryptographic processes. Future Generation Computer Systems\u00a018(6), 747\u2013756 (2002)","journal-title":"Future Generation Computer Systems"},{"unstructured":"Bodei, C.: Security Issues in Process Calculi. PhD thesis, Universit\u00e0 di Pisa (January 2000)","key":"1_CR32"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/3-540-63166-6_15","volume-title":"Computer Aided Verification","author":"D. Bolignano","year":"1997","unstructured":"Bolignano, D.: Towards a mechanization of cryptographic protocol verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 131\u2013142. Springer, Heidelberg (1997)"},{"issue":"3","key":"1_CR34","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1137\/S0097539700377864","volume":"31","author":"M. Boreale","year":"2001","unstructured":"Boreale, M., De Nicola, R., Pugliese, R.: Proof techniques for cryptographic processes. SIAM J. Comput.\u00a031(3), 947\u2013986 (2001)","journal-title":"SIAM J. Comput."},{"key":"1_CR35","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)"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-45719-4_20","volume-title":"Algebraic Methodology and Software Technology","author":"J. Borgstr\u00f6m","year":"2002","unstructured":"Borgstr\u00f6m, J., Nestmann, U.: On bisimulations for the spi calculus. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 287\u2013303. Springer, Heidelberg (2002)"},{"key":"1_CR37","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1098\/rspa.1989.0125","volume":"426","author":"M. Burrows","year":"1989","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication (A preliminary version appeared as Digital Equipment Corporation Systems Research Center report No. 39, February 1989). Proceedings of the Royal Society of London A\u00a0426, 233\u2013271 (1989)","journal-title":"Proceedings of the Royal Society of London A"},{"issue":"3","key":"1_CR38","doi-asserted-by":"crossref","first-page":"423","DOI":"10.3233\/JCS-2005-13304","volume":"13","author":"A. Datta","year":"2005","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security\u00a013(3), 423\u2013482 (2005)","journal-title":"Journal of Computer Security"},{"issue":"1","key":"1_CR39","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/j.entcs.2007.02.012","volume":"172","author":"A. Datta","year":"2007","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (PCL). Electronic Notes in Theoretical Computer Science\u00a0172(1), 311\u2013358 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"DeMillo, R.A., Lynch, N.A., Merritt, M.: Cryptographic protocols. In: 14th Annual ACM Symposium on Theory of Computing, pp. 383\u2013400 (1982)","key":"1_CR40","DOI":"10.1145\/800070.802214"},{"issue":"7","key":"1_CR41","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. Communications of the ACM\u00a024(7), 533\u2013535 (1981)","journal-title":"Communications of the ACM"},{"issue":"12","key":"1_CR42","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"},{"key":"1_CR43","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/978-0-387-35533-7_10","volume-title":"Formal Techniques for Distributed System Development, FORTE\/PSTV","author":"L. Durante","year":"2000","unstructured":"Durante, L., Sisto, R., Valenzano, A.: A state-exploration technique for spi-calculus testing-equivalence verification. In: Formal Techniques for Distributed System Development, FORTE\/PSTV. IFIP Conference Proceedings, vol.\u00a0183, pp. 155\u2013170. Kluwer, Dordrecht (2000)"},{"issue":"2","key":"1_CR44","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1145\/941566.941570","volume":"12","author":"L. Durante","year":"2003","unstructured":"Durante, L., Sisto, R., Valenzano, A.: Automatic testing equivalence verification of spi calculus specifications. ACM Transactions on Software Engineering and Methodology\u00a012(2), 222\u2013284 (2003)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"9","key":"1_CR45","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1109\/32.629493","volume":"23","author":"R. Focardi","year":"1997","unstructured":"Focardi, R., Gorrieri, R.: The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering\u00a023(9), 550\u2013571 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"unstructured":"Freier, A.O., Karlton, P., Kocher, P.C.: The SSL protocol: Version 3.0 (November 1996), http:\/\/www.mozilla.org\/projects\/security\/pki\/nss\/ssl\/draft302.txt","key":"1_CR46"},{"key":"1_CR47","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1016\/0022-0000(84)90070-9","volume":"28","author":"S. Goldwasser","year":"1984","unstructured":"Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences\u00a028, 270\u2013299 (1984)","journal-title":"Journal of Computer and System Sciences"},{"doi-asserted-by":"crossref","unstructured":"Gordon, A.D.: Provable implementations of security protocols. In: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 345\u2013346 (2006)","key":"1_CR48","DOI":"10.1109\/LICS.2006.43"},{"doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. In: 14th IEEE Computer Security Foundations Workshop, pp. 145\u2013159 (June 2001)","key":"1_CR49","DOI":"10.1109\/CSFW.2001.930143"},{"doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. In: 15th IEEE Computer Security Foundations Workshop, pp. 77\u201391 (June 2002)","key":"1_CR50","DOI":"10.1109\/CSFW.2002.1021808"},{"key":"1_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"doi-asserted-by":"crossref","unstructured":"Gray III, J.W., Ip, K.F.E., Lui, K.-S.: Provable security for cryptographic protocols\u2014exact analysis and engineering applications. In: 10th IEEE Computer Security Foundations Workshop, pp. 45\u201358 (1997)","key":"1_CR52","DOI":"10.1109\/CSFW.1997.596784"},{"doi-asserted-by":"crossref","unstructured":"Harkins, D., Carrel, D.: RFC 2409: The Internet Key Exchange (IKE) (November 1998), http:\/\/www.ietf.org\/rfc\/rfc2409.txt","key":"1_CR53","DOI":"10.17487\/rfc2409"},{"doi-asserted-by":"crossref","unstructured":"H\u00fcttel, H.: Deciding framed bisimilarity. In: 4th International Workshop on Verification of Infinite-State Systems (INFINITY 2002), pp. 1\u201320 (August 2002)","key":"1_CR54","DOI":"10.7146\/brics.v9i25.21741"},{"issue":"2","key":"1_CR55","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00197942","volume":"7","author":"R.A. Kemmerer","year":"1994","unstructured":"Kemmerer, R.A., Meadows, C., Millen, J.K.: Three systems for cryptographic protocol analysis. Journal of Cryptology\u00a07(2), 79\u2013130 (1994)","journal-title":"Journal of Cryptology"},{"doi-asserted-by":"crossref","unstructured":"Kohl, J., Neuman, C.: RFC 1510: The Kerberos network authentication service (v5) (September 1993), ftp:\/\/ftp.isi.edu\/in-notes\/rfc1510.txt","key":"1_CR56","DOI":"10.17487\/rfc1510"},{"key":"1_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"unstructured":"Lampson, B.W.: Protection. In: 5th Princeton Conference on Information Sciences and Systems, pp. 437\u2013443 (1971)","key":"1_CR58"},{"doi-asserted-by":"crossref","unstructured":"Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: 2004 IEEE Symposium on Security and Privacy, pp. 71\u201385 (May 2004)","key":"1_CR59","DOI":"10.1109\/SECPRI.2004.1301316"},{"doi-asserted-by":"crossref","unstructured":"Laud, P.: Secrecy types for a simulatable cryptographic library. In: 12th ACM Conference on Computer and Communications Security (CCS 2005), pp. 26\u201335 (November 2005)","key":"1_CR60","DOI":"10.1145\/1102120.1102126"},{"doi-asserted-by":"crossref","unstructured":"Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: 5th ACM Conference on Computer and Communications Security (CCS 1998), pp. 112\u2013121 (1998)","key":"1_CR61","DOI":"10.1145\/288090.288117"},{"key":"1_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"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: Proceedings of the IEEE International Conference on Web Services, pp. 75\u201382 (2005)","key":"1_CR63","DOI":"10.1109\/ICWS.2005.138"},{"doi-asserted-by":"crossref","unstructured":"Lynch, N.: I\/O automaton models and proofs for shared-key communication systems. In: 12th IEEE Computer Security Foundations Workshop, pp. 14\u201329 (1999)","key":"1_CR64","DOI":"10.1109\/CSFW.1999.779759"},{"key":"1_CR65","doi-asserted-by":"crossref","DOI":"10.1201\/9781439821916","volume-title":"Handbook of Applied Cryptography","author":"A.J. Menezes","year":"1996","unstructured":"Menezes, A.J., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)"},{"unstructured":"Merritt, M.J.: Cryptographic Protocols. PhD thesis, Georgia Institute of Technology (February 1983)","key":"1_CR66"},{"key":"1_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-540-24638-1_8","volume-title":"Theory of Cryptography","author":"D. Micciancio","year":"2004","unstructured":"Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol.\u00a02951, pp. 133\u2013151. Springer, Heidelberg (2004)"},{"unstructured":"Miller, S.P., Neuman, B.C., Schiller, J.I., Saltzer, J.H.: Kerberos authentication and authorization system, Project Athena technical plan, section E.2.1. Technical report. MIT (July 1987)","key":"1_CR68"},{"key":"1_CR69","volume-title":"Communicating and Mobile Systems: the \u03c0-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"1_CR70","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0890-5401(92)90009-5","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts I and II. Information and Computation, 100, 1\u201340, 41\u201377 (1992)","journal-title":"Information and Computation"},{"unstructured":"Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-state analysis of SSL 3.0. In: 7th USENIX Security Symposium, pp. 201\u2013216 (January 1998)","key":"1_CR71"},{"issue":"2-3","key":"1_CR72","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"},{"doi-asserted-by":"crossref","unstructured":"Needham, R.M.: Logic and over-simplification. In: 13th Annual IEEE Symposium on Logic in Computer Science, pp. 2\u20133 (1998)","key":"1_CR73","DOI":"10.1109\/LICS.1998.705638"},{"issue":"12","key":"1_CR74","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. Communications of the ACM\u00a021(12), 993\u2013999 (1978)","journal-title":"Communications of the ACM"},{"issue":"1","key":"1_CR75","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/24592.24593","volume":"21","author":"R.M. Needham","year":"1987","unstructured":"Needham, R.M., Schroeder, M.D.: Authentication revisited. Operating Systems Review\u00a021(1), 7 (1987)","journal-title":"Operating Systems Review"},{"issue":"1-2","key":"1_CR76","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":"1_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"468","DOI":"10.1007\/978-3-540-24727-2_33","volume-title":"Foundations of Software Science and Computation Structures","author":"A. Ramanathan","year":"2004","unstructured":"Ramanathan, A., Mitchell, J., Scedrov, A., Teague, V.: Probabilistic bisimulation and equivalence for security analysis of network protocols. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 468\u2013483. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Schneider, S.: Security properties and CSP. In: 1996 IEEE Symposium on Security and Privacy, pp. 174\u2013187 (1996)","key":"1_CR78","DOI":"10.1109\/SECPRI.1996.502680"},{"doi-asserted-by":"crossref","unstructured":"Syverson, P.: Limitations on design principles for public key protocols. In: 1996 IEEE Symposium on Security and Privacy, pp. 62\u201373 (1996)","key":"1_CR79","DOI":"10.1109\/SECPRI.1996.502670"},{"doi-asserted-by":"crossref","unstructured":"Javier Thayer F\u00e1brega, F., Herzog, J.C., Guttman, J.D.: Strand spaces: Why is a security protocol correct? In: 1998 IEEE Symposium on Security and Privacy, pp. 160\u2013171 (May 1998)","key":"1_CR80","DOI":"10.21236\/ADA459060"},{"issue":"1","key":"1_CR81","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1109\/2.108052","volume":"25","author":"T.Y.C. Woo","year":"1992","unstructured":"Woo, T.Y.C., Lam, S.S.: Authentication for distributed systems. Computer\u00a025(1), 39\u201352 (1992)","journal-title":"Computer"},{"issue":"3","key":"1_CR82","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/182110.182113","volume":"28","author":"T.Y.C. Woo","year":"1994","unstructured":"Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. Operating Systems Review\u00a028(3), 24\u201337 (1994)","journal-title":"Operating Systems Review"},{"doi-asserted-by":"crossref","unstructured":"Yao, A.C.: Theory and applications of trapdoor functions. In: 23rd Annual Symposium on Foundations of Computer Science (FOCS 1982), pp. 80\u201391 (1982)","key":"1_CR83","DOI":"10.1109\/SFCS.1982.45"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security Analysis and Design IV"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74810-6_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:24:09Z","timestamp":1605745449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74810-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540748090","9783540748106"],"references-count":83,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74810-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}