{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:07:02Z","timestamp":1736399222281,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540330455"},{"type":"electronic","value":"9783540330462"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11690634_29","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:15:28Z","timestamp":1143555328000},"page":"428-445","source":"Crossref","is-referenced-by-count":12,"title":["Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario"],"prefix":"10.1007","author":[{"given":"Michael","family":"Backes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"M\u00f6dersheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Birgit","family":"Pfitzmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-44929-9_1","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"M. Abadi","year":"2000","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography: The computational soundness of formal encryption. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872, pp. 3\u201322. Springer, Heidelberg (2000)"},{"key":"29_CR2","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., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., He\u00e1m, 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":"29_CR3","doi-asserted-by":"crossref","unstructured":"Backes, M., M\u00f6dersheim, S., Pfitzmann, B., Vigan\u00f2, L.: Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario (Extended Version). Technical Report 502, Department of Computer Science, ETH Zurich (2006), Available at: www.infsec.ethz.ch","DOI":"10.1007\/11690634_29"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. 17th IEEE CSFW (2004)","DOI":"10.1109\/CSFW.2004.1310742"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: Proc. 10th ACM CCS, January 2003, Full version in IACR Cryptology ePrint Archive 2003\/015, pp. 220\u2013230 (2003), http:\/\/eprint.iacr.org\/","DOI":"10.1145\/948138.948140"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-39650-5_16","volume-title":"Computer Security \u2013 ESORICS 2003","author":"M. Backes","year":"2003","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within a simulatable cryptographic library. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol.\u00a02808, pp. 271\u2013290. Springer, Heidelberg (2003)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-540-24638-1_19","volume-title":"Theory of Cryptography","author":"M. Backes","year":"2004","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A general composition theorem for secure reactive systems. In: Naor, M. (ed.) TCC 2004. LNCS, vol.\u00a02951, pp. 336\u2013354. Springer, Heidelberg (2004)"},{"issue":"3","key":"29_CR8","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D. Basin","year":"2005","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A Symbolic Model-Checker for Security Protocols. International Journal of Information Security\u00a04(3), 181\u2013208 (2005)","journal-title":"International Journal of Information Security"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET Purchase Protocols. Journal of Automated Reasoning (to appear)","DOI":"10.1007\/s10817-005-9018-6"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/3-540-44448-3_41","volume-title":"Advances in Cryptology - ASIACRYPT 2000","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Namprempre, C.: Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol.\u00a01976, pp. 531\u2013545. Springer, Heidelberg (2000)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-44448-3_24","volume-title":"Advances in Cryptology - ASIACRYPT 2000","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Rogaway, P.: Encode-then-encipher encryption: How to exploit nonces or redundancy in plaintexts for efficient constructions. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol.\u00a01976, pp. 317\u2013330. Springer, Heidelberg (2000)"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Corin, R., Fournet, C., Gordon, A.: Secure sessions for web services. In: Proc.\u00a0ACM Workshop on Secure Web Services (SWS) (2004)","DOI":"10.1145\/1111348.1111355"},{"key":"29_CR13","first-page":"198","volume-title":"Proc. 31st POPL","author":"K. Bhargavan","year":"2004","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.: A semantics for web service authentication. In: Proc. 31st POPL, pp. 198\u2013209. ACM Press, New York (2004)"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.: Verifying policy-based security for web services. In: Proc. 11th ACM CCS, pp. 268\u2013277 (2004)","DOI":"10.1145\/1030083.1030120"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Pucella, R.: TulaFale: A security tool for web servics. 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)"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. 14th IEEE CSFW, pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"issue":"3","key":"29_CR17","doi-asserted-by":"publisher","first-page":"347","DOI":"10.3233\/JCS-2005-13302","volume":"13","author":"C. Bodei","year":"2005","unstructured":"Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Riis Nielson, H.: Static validation of security protocols. Journal of Computer Security\u00a013(3), 347\u2013390 (2005)","journal-title":"Journal of Computer Security"},{"key":"29_CR18","unstructured":"Box, D., Curbera, F., et al.: Web Services Addressing (WS-Addressing) (August 2004)"},{"key":"29_CR19","unstructured":"Box, D., Ehnebuske, D., Kakivaya, G., Layman, A., Mendelsohn, N., Nielsen, H.F., Thatte, S., Winer, D.: Simple object access protocol (SOAP) 1.1 (May 2000)"},{"key":"29_CR20","unstructured":"Canetti, R., Herzog, J.: Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). Cryptology ePrint Archive, Report 2004\/334 (2004)"},{"key":"29_CR21","unstructured":"Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Mantovani, J., M\u00f6dersheim, S., Vigneron, L.: A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In: Proc. Workshop on Specification and Automated Processing of Security Requirements (SAPS 2004), pp. 193\u2013205. Austrian Computer Society (2004)"},{"key":"29_CR22","unstructured":"Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0, 17 November\u00a0(1997)"},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-36575-3_8","volume-title":"Programming Languages and Systems","author":"H. Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, pp. 99\u2013113. Springer, Heidelberg (2003)"},{"key":"29_CR24","unstructured":"Davis, D., Ferris, C., Gajjala, V., Gavrylyuk, K., Gudgin, M., Kaler, C., Langworthy, D., Moroney, M., Nadalin, A., Roots, J., Storey, T., Vishwanath, T., Walte, D.: Secure WS-ReliableMessaging scenarios (April 2005), ftp:\/\/www6.software.ibm.com\/software\/developer\/library\/ws-rmseconscenario.doc"},{"issue":"2","key":"29_CR25","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory\u00a029(2), 198\u2013208 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"key":"29_CR26","unstructured":"Donovan, B., Norris, P., Lowe, G.: Analyzing a library of security protocols using Casper and FDR. In: Proc. Workshop on Formal Methods and Security Protocols (FMSP 1999) (1999)"},{"key":"29_CR27","unstructured":"Ferguson, D.F., Storey, T., Lovering, B., Shewchuk, J.: Secure, reliable, transacted Web Services \u2013 architecture and composition (October 2003), Available at: http:\/\/www-106.ibm.com\/developerworks\/webservices\/library\/ws-securtrans\/"},{"key":"29_CR28","unstructured":"Ferris, C., Langworthy, D., et al.: Web Services Reliable Messaging Protocol (WS-ReliableMessaging) (February 2005)"},{"key":"29_CR29","doi-asserted-by":"crossref","unstructured":"Gordon, A., Pucella, R.: Validating a web service security abstraction by typing. In: Proc. 1st ACM Workshop on XML Security, pp. 18\u201329 (2002)","DOI":"10.1145\/764792.764797"},{"issue":"1","key":"29_CR30","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.entcs.2005.06.004","volume":"135","author":"A. Gotsman","year":"2005","unstructured":"Gotsman, A., Massacci, F., Pistore, M.: Towards an Independent Semantics and Verification Technology for the HLPSL Specification Language. Electronic Notes in Theoretical Computer Science\u00a0135(1), 59\u201377 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"29_CR31","first-page":"54","volume-title":"Proc.\u00a0ACM Workshop on Secure Web Services (SWS)","author":"T. Gro\u00df","year":"2005","unstructured":"Gro\u00df, T., Pfitzmann, B., Sadeghi, A.-R.: Proving a WS-Federation Passive Requestor Profile with a Browser Model. In: Proc.\u00a0ACM Workshop on Secure Web Services (SWS), pp. 54\u201364. ACM Press, New York (2005)"},{"key":"29_CR32","unstructured":"Gudgin, M., Nadalin, A., et al.: Web Services Secure Conversation Language (WS-SecureConversation) (February 2005)"},{"key":"29_CR33","unstructured":"Gudgin, M., Nadalin, A., et al.: Web Services Trust Language (WS-Trust (February 2005)"},{"key":"29_CR34","unstructured":"Hur, M., Johnson, R.D., Medvinsky, A., Rouskov, Y., Spellman, J., Weeden, S., Nadalin, A.: Passive Requestor Federation Interop Scenario, Version 0.4 (February 2004), ftp:\/\/www6.software.ibm.com\/software\/developer\/library\/ws-fpscenario2.doc"},{"key":"29_CR35","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-44404-1_10","volume-title":"Logic for Programming and Automated Reasoning","author":"F. Jacquemard","year":"2000","unstructured":"Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and verifying security protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 131\u2013160. Springer, Heidelberg (2000)"},{"key":"29_CR36","doi-asserted-by":"crossref","unstructured":"Kaler, C., et al.: Web Services Security (WS-Security), version 1.0 (April 2002)","DOI":"10.1016\/S1361-3723(02)00407-4"},{"key":"29_CR37","doi-asserted-by":"crossref","unstructured":"Kleiner, E., Roscoe, A.: On the relationship of traditional and Web Services Security protocols. In: Proceedings of the XXI Mathematical Foundations of Programming Semantics (MFPS 2005). Electronic Notes in Theoretical Computer Science (to appear)","DOI":"10.1016\/j.entcs.2005.11.074"},{"key":"29_CR38","doi-asserted-by":"crossref","unstructured":"Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. 25th IEEE Symposium on Security & Privacy, pp. 71\u201385 (2004)","DOI":"10.1109\/SECPRI.2004.1301316"},{"key":"29_CR39","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Proc. 10th IEEE CSFW, pp. 31\u201343 (1997)","DOI":"10.1109\/CSFW.1997.596782"},{"key":"29_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"29_CR41","doi-asserted-by":"publisher","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"D. Song","year":"2001","unstructured":"Song, D., Berezin, S., Perrig, A.: Athena: a novel approach to efficient automatic security protocol analysis. Journal of Computer Security\u00a09, 47\u201374 (2001)","journal-title":"Journal of Computer Security"},{"key":"29_CR42","unstructured":"Turuani, M.: S\u00e9curit\u00e9 des Protocoles Cryptographiques: D\u00e9cidabilit\u00e9 et Complexit\u00e9. Phd, Universit\u00e9 Henri Poincar\u00e9, Nancy (December 2003)"},{"key":"29_CR43","doi-asserted-by":"crossref","unstructured":"Vigan\u00f2, L.: Automated Security Protocol Analysis with the AVISPA Tool. In: In Proceedings of the XXI Mathematical Foundations of Programming Semantics (MFPS 2005). Electronic Notes in Theoretical Computer Science (to appear)","DOI":"10.1016\/j.entcs.2005.11.052"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11690634_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T04:53:58Z","timestamp":1736312038000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11690634_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540330455","9783540330462"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/11690634_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}