{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:52:47Z","timestamp":1743043967538,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540689133"},{"type":"electronic","value":"9783540689140"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-68914-0_19","type":"book-chapter","created":{"date-parts":[[2008,5,26]],"date-time":"2008-05-26T08:58:06Z","timestamp":1211792286000},"page":"309-327","source":"Crossref","is-referenced-by-count":9,"title":["Analysis of EAP-GPSK Authentication Protocol"],"prefix":"10.1007","author":[{"given":"John C.","family":"Mitchell","sequence":"first","affiliation":[]},{"given":"Arnab","family":"Roy","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Rowe","sequence":"additional","affiliation":[]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Aboba, B., Blunk, L., Vollbrecht, J., Carlson, J.: Extensible Authentication Protocol. RFC 3748 (2004)","DOI":"10.17487\/rfc3748"},{"key":"19_CR2","unstructured":"Clancy, T., Tschofenig, H.: EAP Generalized Pre-Shared Key (EAP-GPSK) (work in progress) (2007), http:\/\/www.ietf.org\/internet-drafts\/draft-ietf-emu-eap-gpsk-05.txt"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/11523468_2","volume-title":"Automata, Languages and Programming","author":"A. Datta","year":"2005","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 16\u201329. Springer, Heidelberg (2005)"},{"key":"19_CR4","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1109\/CSFW.2006.9","volume-title":"Proceedings of 19th IEEE Computer Security Foundations Workshop","author":"A. Datta","year":"2006","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: Proceedings of 19th IEEE Computer Security Foundations Workshop, pp. 321\u2013334. IEEE, Los Alamitos (2006)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","first-page":"147","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1996","unstructured":"Dill, D.L.: The Mur\u03c6 Verification System. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 147\u2013158. Springer, Heidelberg (1996)"},{"key":"19_CR6","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 (1997)"},{"key":"19_CR7","unstructured":"Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-State Analysis of SSL 3.0. In: SSYM 1998: Proceedings of the 7th conference on USENIX Security Symposium, 1998, Berkeley, CA, USA, pp. 16\u201316. USENIX Association (1998)"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1145\/1023646.1023655","volume-title":"WiSe 2004: Proceedings of the 3rd ACM Workshop on Wireless Security","author":"C. He","year":"2004","unstructured":"He, C., Mitchell, J.C.: Analysis of the 802.11i 4-Way Handshake. In: WiSe 2004: Proceedings of the 3rd ACM Workshop on Wireless Security, pp. 43\u201350. ACM, New York (2004)"},{"key":"19_CR9","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). Electron. Notes Theor. Comput. Sci.\u00a0172, 311\u2013358 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"19_CR10","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1109\/CSFW.1994.315945","volume-title":"Proceedings of 7th IEEE Computer Security Foundations Workshop","author":"C. Meadows","year":"1994","unstructured":"Meadows, C.: A model of computation for the NRL protocol analyzer. In: Proceedings of 7th IEEE Computer Security Foundations Workshop, pp. 84\u201389. IEEE, Los Alamitos (1994)"},{"key":"19_CR11","volume-title":"Modelling and Analysis of Security Protocols","author":"P. Ryan","year":"2000","unstructured":"Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, A.: Modelling and Analysis of Security Protocols. Addison-Wesley Publishing Co., Reading (2000)"},{"key":"19_CR12","first-page":"160","volume-title":"Proceedings of the 1998 IEEE Symposium on Security and Privacy","author":"F.J.T. F\u00e1brega","year":"1998","unstructured":"F\u00e1brega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy, Oakland, CA, pp. 160\u2013171. IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"19_CR13","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, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0055875","volume-title":"Computer Security \u2013 ESORICS 98","author":"G. Bella","year":"1998","unstructured":"Bella, G., Paulson, L.C.: Kerberos version IV: Inductive analysis of the secrecy goals. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol.\u00a01485, pp. 361\u2013375. Springer, Heidelberg (1998)"},{"key":"19_CR15","first-page":"175","volume-title":"Fifteenth Computer Security Foundations Workshop \u2014 CSFW-15","author":"F. Butler","year":"2002","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A Formal Analysis of Some Properties of Kerberos 5 Using MSR. In: Fifteenth Computer Security Foundations Workshop \u2014 CSFW-15, Cape Breton, NS, Canada, pp. 175\u2013190. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Software Security - Theories and Systems","author":"F. Butler","year":"2004","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: Verifying confidentiality and authentication in kerberos 5. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol.\u00a03233, pp. 1\u201324. Springer, Heidelberg (2004)"},{"key":"19_CR17","unstructured":"Cervesato, I., Jaggard, A., Scedrov, A., Tsay, J.K., Walstad, C.: Breaking and fixing public-key kerberos (Technical report)"},{"key":"19_CR18","volume-title":"CSFW-18","author":"I. Cervasato","year":"2005","unstructured":"Cervasato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution. In: CSFW-18, IEEE Computer Society, Los Alamitos (2005)"},{"key":"19_CR19","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, 423\u2013482 (2005)","journal-title":"Journal of Computer Security"},{"key":"19_CR20","unstructured":"Hasebe, K., Okada, M.: Non-monotonic properties for proving correctness in a framework of compositional logic. In: Foundations of Computer Security Workshop, pp. 97\u2013113 (2004)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/978-3-540-37621-7_4","volume-title":"Software Security - Theories and Systems","author":"K. Hasebe","year":"2004","unstructured":"Hasebe, K., Okada, M.: Inferences on honesty in compositional logic for security analysis. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol.\u00a03233, pp. 65\u201386. Springer, Heidelberg (2004)"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, J.C.: A modular correctness proof of ieee 802.11i and tls. In: ACM Conference on Computer and Communications Security, pp. 2\u201315 (2005)","DOI":"10.1145\/1102120.1102124"},{"key":"19_CR23","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, 103\u2013127 (2002)","journal-title":"Journal of Cryptology"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. Cryptology ePrint Archive, Report 2003\/015 (2003)","DOI":"10.1145\/948138.948140"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1007\/11523468_53","volume-title":"Automata, Languages and Programming","author":"M. Baudet","year":"2005","unstructured":"Baudet, M., Cortier, V., Kremer, S.: Computationally Sound Implementations of Equational Theories against Passive Adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 652\u2013663. Springer, Heidelberg (2005)"},{"key":"19_CR26","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)"},{"key":"19_CR27","unstructured":"Herzog, J.: Computational Soundness for Standard Assumptions of Formal Cryptography. PhD thesis, MIT (2004)"},{"key":"19_CR28","first-page":"170","volume":"18","author":"P. Ad\u00e3o","year":"2005","unstructured":"Ad\u00e3o, P., Bana, G., Scedrov, A.: Computational and information-theoretic soundness and completeness of formal encryption. CSFW\u00a018, 170\u2013184 (2005)","journal-title":"CSFW"},{"key":"19_CR29","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)"},{"key":"19_CR30","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1109\/CSFW.2003.1212717","volume-title":"Proceedings of 16th Computer Science Foundation Workshop","author":"B. Warinschi","year":"2003","unstructured":"Warinschi, B.: A computational analysis of the Needham-Schroeder(-Lowe) protocol. In: Proceedings of 16th Computer Science Foundation Workshop, pp. 248\u2013262. ACM Press, New York (2003)"},{"key":"19_CR31","unstructured":"Roy, A., Datta, A., Derek, A., Mitchell, J.C., Seifert, J.P.: Secrecy analysis in Protocol Composition Logic. In: Proceedings of 11th Annual Asian Computing Science Conference (to appear, 2006)"},{"key":"19_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-540-74835-9_15","volume-title":"Computer Security \u2013 ESORICS 2007","author":"A. Roy","year":"2007","unstructured":"Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive proofs of computational secrecy. In: Biskup, J., L\u00f3pez, J. (eds.) ESORICS 2007. LNCS, vol.\u00a04734, pp. 219\u2013234. Springer, Heidelberg (2007)"},{"key":"19_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-540-78663-4_21","volume-title":"3rd Symposium on Trustworthy Global Computing, TGC 2007","author":"A. Roy","year":"2008","unstructured":"Roy, A., Datta, A., Mitchell, J.C.: Formal proofs of cryptographic security of Diffie-Hellman-based protocols. In: 3rd Symposium on Trustworthy Global Computing, TGC 2007. LNCS, vol.\u00a04912, pp. 312\u2013329. Springer, Heidelberg (2008)"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive trace properties for computational security. In: WITS (2007)","DOI":"10.1007\/978-3-540-74835-9_15"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Dierks, T., Rescorla, E.: The Transport Layer Security (TLS) Protocol Version 1.1. RFC 4346 (2006)","DOI":"10.17487\/rfc4346"},{"key":"19_CR36","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/276698.276741","volume-title":"STOC 1998: Proceedings of the thirtieth annual ACM symposium on Theory of computing","author":"R. Canetti","year":"1998","unstructured":"Canetti, R., Goldreich, O., Halevi, S.: The random oracle methodology, revisited (preliminary version). In: STOC 1998: Proceedings of the thirtieth annual ACM symposium on Theory of computing, pp. 209\u2013218. ACM, New York (1998)"},{"key":"19_CR37","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/CSFW.2001.930150","volume-title":"Proceedings of 14th IEEE Computer Security Foundations Workshop","author":"N. Durgin","year":"2001","unstructured":"Durgin, N., Mitchell, J.C., Pavlovic, D.: A compositional logic for protocol correctness. In: Proceedings of 14th IEEE Computer Security Foundations Workshop, pp. 241\u2013255. IEEE, Los Alamitos (2001)"},{"key":"19_CR38","doi-asserted-by":"crossref","first-page":"677","DOI":"10.3233\/JCS-2003-11407","volume":"11","author":"N. Durgin","year":"2003","unstructured":"Durgin, N., Mitchell, J.C., Pavlovic, D.: A compositional logic for proving security properties of protocols. Journal of Computer Security\u00a011, 677\u2013721 (2003)","journal-title":"Journal of Computer Security"},{"key":"19_CR39","first-page":"109","volume-title":"CSFW-16","author":"A. Datta","year":"2003","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system for security protocols and its logical formalization. In: CSFW-16, pp. 109\u2013125. IEEE, Los Alamitos (2003)"},{"key":"19_CR40","doi-asserted-by":"crossref","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Secure protocol composition. In: Proceedings of 19th Annual Conference on Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol.\u00a083 (2004)","DOI":"10.1016\/S1571-0661(03)50011-1"},{"key":"19_CR41","first-page":"30","volume-title":"CSFW-17","author":"A. Datta","year":"2004","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Abstraction and refinement in protocol derivation. In: CSFW-17, pp. 30\u201345. IEEE, Los Alamitos (2004)"},{"key":"19_CR42","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)"}],"container-title":["Lecture Notes in Computer Science","Applied Cryptography and Network Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68914-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,18]],"date-time":"2023-05-18T14:12:19Z","timestamp":1684419139000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68914-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540689133","9783540689140"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68914-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}