{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T06:48:20Z","timestamp":1709275700241},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"6","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2008,10]]},"abstract":"WS-SecurityPolicy is a declarative language for configuring web services security mechanisms. We describe a formal semantics for WS-SecurityPolicy and propose a more abstract language for specifying secure links between web services and their clients. We present the architecture and implementation of tools that (1) compile policy files from link specifications, and (2) verify by invoking a theorem prover whether a set of policy files run by any number of senders and receivers correctly implements the goals of a link specification, in spite of active attackers. Policy-driven web services implementations are prone to the usual subtle vulnerabilities associated with cryptographic protocols; our tools help prevent such vulnerabilities. We can verify policies when first compiled from link specifications, and also re-verify policies against their original goals after any modifications during deployment. Moreover, we present general security theorems for all configurations that rely on compiled policies.<\/jats:p>","DOI":"10.1145\/1391956.1391957","type":"journal-article","created":{"date-parts":[[2008,11,6]],"date-time":"2008-11-06T13:49:43Z","timestamp":1225979383000},"page":"1-59","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Verifying policy-based web services security"],"prefix":"10.1145","volume":"30","author":[{"given":"Karthikeyan","family":"Bhargavan","sequence":"first","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2008,10,30]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2005.25"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1237500.1237504"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.005"},{"key":"e_1_2_1_5_1","volume-title":"Tech. Rep. MSR--TR--2004--84, Microsoft Research. Nov.","author":"Bhargavan K.","year":"2005","unstructured":"Bhargavan , K. , Fournet , C. , and Gordon , A. D . 2005 b. Verifying policy-based security for web services. Tech. Rep. MSR--TR--2004--84, Microsoft Research. Nov. Bhargavan, K., Fournet, C., and Gordon, A. D. 2005b. Verifying policy-based security for web services. Tech. Rep. MSR--TR--2004--84, Microsoft Research. Nov."},{"key":"e_1_2_1_6_1","unstructured":"Bhargavan K. Fournet C. and Gordon A. D. 2006b. Policy advisor for WSE 3.0. In Web Service Security: Scenarios patterns and implementation guidance for Web Services Enhancements (WSE) 3.0. Microsoft Press 324--330. Bhargavan K. Fournet C. and Gordon A. D. 2006b. Policy advisor for WSE 3.0. In Web Service Security: Scenarios patterns and implementation guidance for Web Services Enhancements (WSE) 3.0. Microsoft Press 324--330."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11841197_6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1103022.1103024"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO'03)","volume":"3188","author":"Bhargavan K.","unstructured":"Bhargavan , K. , Fournet , C. , Gordon , A. D. , and Pucella , R . 2004. TulaFale: A security tool for web services . In Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO'03) . Lecture Notes in Computer Science , vol. 3188 . Springer-Verlag, New York, 197--222. Tool download available from http:\/\/Securing.WS. Bhargavan, K., Fournet, C., Gordon, A. D., and Pucella, R. 2004. TulaFale: A security tool for web services. In Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO'03). Lecture Notes in Computer Science, vol. 3188. Springer-Verlag, New York, 197--222. Tool download available from http:\/\/Securing.WS."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368330"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.32"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/647171.716095"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.8"},{"key":"e_1_2_1_15_1","unstructured":"Box D. Christensen E. Curbera F. Ferguson D. Frey J. Hadley M. Kaler C. Langworthy D. Leymann F. Lovering B. Lucco S. Millet S. Mukhi N. Nottingham M. Orchard D. Shewchuk J. Sindambiwe E. Storey T. Weerawarana S. and Winkler S. 2004. Web Services Addressing (WS-Addressing). W3C Submission. Box D. Christensen E. Curbera F. Ferguson D. Frey J. Hadley M. Kaler C. Langworthy D. Leymann F. Lovering B. Lucco S. Millet S. Mukhi N. Nottingham M. Orchard D. Shewchuk J. Sindambiwe E. Storey T. Weerawarana S. and Winkler S. 2004. Web Services Addressing (WS-Addressing). W3C Submission."},{"key":"e_1_2_1_16_1","unstructured":"Box D. Curbera F. Hondo M. Kaler C. Langworthy D. Nadalin A. Nagaratnam N. Nottingham M. von Riegen C. and Shewchuk J. 2003a. Web services policy framework (WS-Policy). Box D. Curbera F. Hondo M. Kaler C. Langworthy D. Nadalin A. Nagaratnam N. Nottingham M. von Riegen C. and Shewchuk J. 2003a. Web services policy framework (WS-Policy)."},{"key":"e_1_2_1_17_1","unstructured":"Box D. Hondo M. Kaler C. Maruyama H. Nadalin A. Nagaratnam N. Patrick P. von Riegen C. and Shewchuk J. 2003b. Web services policy assertions language (WS-PolicyAssertions). Box D. Hondo M. Kaler C. Maruyama H. Nadalin A. Nagaratnam N. Patrick P. von Riegen C. and Shewchuk J. 2003b. Web services policy assertions language (WS-PolicyAssertions)."},{"key":"e_1_2_1_18_1","unstructured":"Della-Libera G. Hallam-Baker P. Hondo M. Janczuk T. Kaler C. Maruyama H. Nagaratnam N. Nash A. Philpott R. Prafullchandra H. Shewchuk J. Waingold E. and Zolfonoon R. 2002. Web services security policy language (WS-SecurityPolicy). Version 1.0. Della-Libera G. Hallam-Baker P. Hondo M. Janczuk T. Kaler C. Maruyama H. Nagaratnam N. Nash A. Philpott R. Prafullchandra H. Shewchuk J. Waingold E. and Zolfonoon R. 2002. Web services security policy language (WS-SecurityPolicy). Version 1.0."},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Dierks T. and Rescorla E. 2006. The Transport Layer Security (TLS) Protocol Version 1.1. RFC 4346 Internet Engineering Task Force Proposed Standard. Dierks T. and Rescorla E. 2006. The Transport Layer Security (TLS) Protocol Version 1.1. RFC 4346 Internet Engineering Task Force Proposed Standard.","DOI":"10.17487\/rfc4346"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Eastlake D. Reagle J. Imamura T. Dillaway B. and Simon E. 2002a. XML Encryption Syntax and Processing. W3C Recommendation. Eastlake D. Reagle J. Imamura T. Dillaway B. and Simon E. 2002a. XML Encryption Syntax and Processing. W3C Recommendation.","DOI":"10.17487\/rfc3075"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Eastlake D. Reagle J. Solo D. Bartel M. Boyer J. Fox B. LaMacchia B. and Simon E. 2002b. XML-Signature Syntax and Processing. W3C Recommendation. Eastlake D. Reagle J. Solo D. Bartel M. Boyer J. Fox B. LaMacchia B. and Simon E. 2002b. XML-Signature Syntax and Processing. W3C Recommendation.","DOI":"10.17487\/rfc3075"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/959088.959090"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0058-1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0052-x"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the Workshop on Issues in the Theory of Security (WITS'02)","author":"Lowe G.","year":"2002","unstructured":"Lowe , G. 2002 . Analyzing protocols subject to guessing attacks . In Proceedings of the Workshop on Issues in the Theory of Security (WITS'02) . Portland, Oregon. Lowe, G. 2002. Analyzing protocols subject to guessing attacks. In Proceedings of the Workshop on Issues in the Theory of Security (WITS'02). Portland, Oregon."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the Southern African Telecommunication Networks and Applications Conference (SATNAC).","author":"Lukell S.","unstructured":"Lukell , S. , Veldman , C. , and Hutchison , A. C. M. 2003. Automated attack analysis and code generation in a multi-dimensional security protocol engineering framework . In Proceedings of the Southern African Telecommunication Networks and Applications Conference (SATNAC). Lukell, S., Veldman, C., and Hutchison, A. C. M. 2003. Automated attack analysis and code generation in a multi-dimensional security protocol engineering framework. In Proceedings of the Southern African Telecommunication Networks and Applications Conference (SATNAC)."},{"key":"e_1_2_1_28_1","volume-title":"Web Services Enhancements (WSE) 2.0","author":"Microsoft Corporation 2004.","unstructured":"Microsoft Corporation 2004. Web Services Enhancements (WSE) 2.0 . Microsoft Corporation . Microsoft Corporation 2004. Web Services Enhancements (WSE) 2.0. Microsoft Corporation."},{"key":"e_1_2_1_29_1","unstructured":"Muller F. and Millen J. 2001. Cryptographic protocol generation from CAPSL. Tech. Rep. SRI--CSL--01--07 SRI. Muller F. and Millen J. 2001. Cryptographic protocol generation from CAPSL. Tech. Rep. SRI--CSL--01--07 SRI."},{"key":"e_1_2_1_30_1","unstructured":"Nadalin A. Griffin P. Kaler C. Hallam-Baker P. and Monzillo R. 2004a. Web Services Security: UsernameToken Profile 1.0. OASIS Standard. Nadalin A. Griffin P. Kaler C. Hallam-Baker P. and Monzillo R. 2004a. Web Services Security: UsernameToken Profile 1.0. OASIS Standard."},{"key":"e_1_2_1_31_1","unstructured":"Nadalin A. Kaler C. Hallam-Baker P. and Monzillo R. 2004b. Web Services Security: SOAP Message Security 1.0 (WS-Security 2004). OASIS Standard. Nadalin A. Kaler C. Hallam-Baker P. and Monzillo R. 2004b. Web Services Security: SOAP Message Security 1.0 (WS-Security 2004). OASIS Standard."},{"key":"e_1_2_1_32_1","unstructured":"Nadalin A. Kaler C. Hallam-Baker P. and Monzillo R. 2006. Web Services Security: SOAP Message Security 1.1 (WS-Security 2004). OASIS Standard. Nadalin A. Kaler C. Hallam-Baker P. and Monzillo R. 2006. Web Services Security: SOAP Message Security 1.1 (WS-Security 2004). OASIS Standard."},{"key":"e_1_2_1_33_1","unstructured":"Nadalin A. Goodner M. Gudgin M. Barbir A. and Granqvist H. 2007. WS-SecurityPolicy 1.2. OASIS Standard. Nadalin A. Goodner M. Gudgin M. Barbir A. and Granqvist H. 2007. WS-SecurityPolicy 1.2. OASIS Standard."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 13th Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science. Springer-Verlag","author":"Perrig A.","unstructured":"Perrig , A. , Song , D. , and Phan , D . 2001. AGVI -- Automatic generation, verification, and implementation of security protocols . In Proceedings of the 13th Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science. Springer-Verlag , New York, 241--245. Perrig, A., Song, D., and Phan, D. 2001. AGVI -- Automatic generation, verification, and implementation of security protocols. In Proceedings of the 13th Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science. Springer-Verlag, New York, 241--245."},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the 18th International Conference on Advanced Information Networking and Applications (AINA","volume":"1","author":"Pozza D.","year":"2004","unstructured":"Pozza , D. , Sisto , R. , and Durante , L . 2004. Spi2Java: automatic cryptographic protocol Java code generation from spi calculus . In Proceedings of the 18th International Conference on Advanced Information Networking and Applications (AINA 2004 ). Vol. 1 . 400--405. Pozza, D., Sisto, R., and Durante, L. 2004. Spi2Java: automatic cryptographic protocol Java code generation from spi calculus. In Proceedings of the 18th International Conference on Advanced Information Networking and Applications (AINA 2004). Vol. 1. 400--405."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009386.1010163"},{"key":"e_1_2_1_38_1","unstructured":"W3C. 1999. XML Path Language (XPath) Version 1.0. W3C. W3C Recommendation. W3C. 1999. XML Path Language (XPath) Version 1.0. W3C. W3C Recommendation."},{"key":"e_1_2_1_39_1","unstructured":"W3C. 2003. SOAP Version 1.2. W3C. W3C Recommendation. W3C. 2003. SOAP Version 1.2. W3C. W3C Recommendation."},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. IEEE Computer Society Press","author":"Woo T.","unstructured":"Woo , T. and Lam , S . 1993. A semantic model for authentication protocols . In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. IEEE Computer Society Press , Los Alamitos, CA, 178--194. Woo, T. and Lam, S. 1993. A semantic model for authentication protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, 178--194."},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. IEEE Computer Society Press","author":"Zheng L.","unstructured":"Zheng , L. , Chong , S. , Myers , A. C. , and Zdancewic , S . 2003. Using replication and partitioning to build secure distributed systems . In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. IEEE Computer Society Press , Los Alamitos, CA, 236--250. Zheng, L., Chong, S., Myers, A. C., and Zdancewic, S. 2003. Using replication and partitioning to build secure distributed systems. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, 236--250."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1391956.1391957","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T09:46:01Z","timestamp":1672307161000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1391956.1391957"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10]]},"references-count":41,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2008,10]]}},"alternative-id":["10.1145\/1391956.1391957"],"URL":"https:\/\/doi.org\/10.1145\/1391956.1391957","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,10]]},"assertion":[{"value":"2005-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-10-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}