{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T17:00:05Z","timestamp":1792170005529,"version":"4.4.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2005,10,1]],"date-time":"2005-10-01T00:00:00Z","timestamp":1128124800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2005,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>An XML web service is, to a first approximation, an RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. We consider the problem of authenticating requests and responses at the SOAP-level, rather than relying on transport-level security. We propose a security abstraction, inspired by earlier work on secure RPC, in which the methods exported by a web service are annotated with one of three security levels: none, authenticated, or both authenticated and encrypted. We model our abstraction as an object calculus with primitives for defining and calling web services. We describe the semantics of our object calculus by translating to a lower level language with primitives for message passing and cryptography. To validate our semantics, we embed correspondence assertions that specify the correct authentication of requests and responses. By appeal to the type theory for cryptographic protocols of Gordon and Jeffrey's Cryptyc, we verify the correspondence assertions simply by typing. Finally, we describe an implementation of our semantics via custom SOAP headers.<\/jats:p>","DOI":"10.1007\/s00165-004-0058-1","type":"journal-article","created":{"date-parts":[[2005,5,2]],"date-time":"2005-05-02T06:02:46Z","timestamp":1115013766000},"page":"277-318","source":"Crossref","is-referenced-by-count":16,"title":["Validating a web service security abstraction by typing"],"prefix":"10.1145","volume":"17","author":[{"given":"Andrew D.","family":"Gordon","sequence":"first","affiliation":[{"name":"Microsoft Research, Roger Needham Building, 7 J J Thomson Ave, CB3 0FB, Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Riccardo","family":"Pucella","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"p_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"Abadi M","year":"1996"},{"key":"p_2","first-page":"105","volume-title":"13th IEEE symposium on logic in computer science (LICS'98)","author":"Abadi M","year":"1998"},{"key":"p_3","first-page":"74","volume-title":"IEEE computer society symposium on research in security and privacy","author":"Abadi M","year":"1999"},{"key":"p_4","first-page":"302","volume-title":"27th ACM symposium on principles of programming languages (POPL'00)","author":"Abadi M","year":"2000"},{"key":"p_5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2740","article-title":"A calculus for cryptographic protocols: the spi calculus","volume":"148","author":"Abadi M","year":"1999","journal-title":"Inf Comput"},{"key":"p_6","volume-title":"Web services security (WS-Security), version 1.0. Available from http:\/\/msdn.microsoft.com\/library\/ en-us\/dnglobspec\/html\/ws-security.asp","author":"Atkinson B","year":"2002"},{"key":"p_7","first-page":"15","volume-title":"Proceedings of the IEEE symposium on security and privacy. IEEE Computer Society Press","author":"Balfanz D","year":"2000"},{"key":"p_9","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1145\/964001.964018","volume-title":"31st ACM symposium on principles of programming languages (POPL'04)","author":"Bhargavan K","year":"2004"},{"issue":"1","key":"p_10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/214451.214452","article-title":"Secure communication using remote procedure calls","volume":"3","author":"Birrell AD","year":"1985","journal-title":"ACM Trans Comput Syst"},{"key":"p_11","volume-title":"Essential COM","author":"Box D","year":"1997"},{"key":"p_12","volume-title":"Simple object access protocol (SOAP) 1.1. Available from http:\/\/www.w3.org\/TR\/SOAP","author":"Box D","year":"2000"},{"key":"p_13","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0304-3975(99)00231-5","article-title":"Mobile ambients","volume":"240","author":"Cardelli L","year":"2000","journal-title":"Theor Comput Sci"},{"key":"p_14","volume-title":"Web services description language (WSDL) 1.2. Available from http:\/\/www.w3.org\/TR\/2002\/ WD-wsdl12-20020709","author":"Christensen E","year":"2002"},{"issue":"2","key":"p_15","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/s102070100009","article-title":"Securing SOAP e-services","volume":"1","author":"Damiani E","year":"2002","journal-title":"Int J Inf Sec (IJIS)"},{"key":"p_16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/3-540-48749-2_6","volume-title":"Secure internet programming","author":"De Nicola R","year":"1999"},{"key":"p_17","article-title":"On the security of public key protocols","author":"Dolev D","year":"1983","journal-title":"IEEE Trans Inf Theo IT-29(2):198-208"},{"key":"p_18","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1109\/CSFW.2002.1021819","volume-title":"15th IEEE computer security foundations workshop","author":"Duggan D","year":"2002"},{"key":"p_19","first-page":"161","volume-title":"Proceedings of network and distributed system security 2001 (NDSS2001)","author":"Eronen P","year":"2001"},{"key":"p_20","volume-title":"Google Web APIs (beta)","author":"Google","year":"2002"},{"key":"p_21","first-page":"77","volume-title":"IEEE Computer Society Press","author":"Gordon AD","year":"2002"},{"issue":"4","key":"p_22","doi-asserted-by":"crossref","first-page":"451","DOI":"10.3233\/JCS-2003-11402","article-title":"Authenticity by typing for security protocols","volume":"11","author":"Gordon AD","year":"2003","journal-title":"J Comput Sec"},{"key":"p_23","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1016\/S0304-3975(02)00333-X","article-title":"Typing correspondence assertions for communication protocols","volume":"300","author":"Gordon AD","year":"2003","journal-title":"Theor Comput Sci"},{"key":"p_24","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/764792.764797","volume-title":"2002 ACM workshop on XML security","author":"Gordon AD","year":"2002"},{"key":"p_25","first-page":"248","volume-title":"28th ACM symposium on principles of programming languages (POPL'01)","author":"Gordon AD","year":"2001"},{"key":"p_26","volume-title":"Proceedings HLCL'98","author":"Hennessy M","year":"1998"},{"key":"p_27","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/3-540-45500-0_3","volume-title":"Fourth international symposium on theoretical aspects of computer software (TACS2001)","volume":"2215","author":"Hoshina D","year":"2001"},{"key":"p_28","volume-title":"Security in a web services world: A proposed architecture and roadmap. White paper available from http:\/\/msdn.microsoft.com\/ library\/en-us\/dnwssecur\/html\/securitywhitepaper.asp","author":"IBM Corporation and Microsoft Corporation","year":"2002"},{"key":"p_29","first-page":"132","volume-title":"ACM","author":"Igarashi A","year":"1999"},{"issue":"4","key":"p_30","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1145\/138873.138874","article-title":"Authentication in distributed systems: theory and practice","volume":"10","author":"Lampson B","year":"1992","journal-title":"ACM Trans Comput Syst"},{"key":"p_31","volume-title":"Developing secure distributed systems with CORBA","author":"Lang U","year":"2002"},{"key":"p_32","volume-title":"Communicating and mobile systems: the \u03c0-calculus","author":"Milner R","year":"1999"},{"key":"p_33","first-page":"695","volume-title":"25th International colloquium on automata, languages, and programming (ICALP'98), vol 1443 of Lecture Notes in Computer Science","author":"Sewell P","year":"1998"},{"key":"p_34","first-page":"23","volume-title":"Proceedings of the ACM symposium on access control models and technologies","author":"Sirer EG","year":"2002"},{"key":"p_35","first-page":"211","volume-title":"IEEE computer society symposium on research in security and privacy","author":"van Doorn L","year":"1996"},{"issue":"1","key":"p_36","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/174613.174614","article-title":"Authentication in the Taos operating system","volume":"12","author":"Wobber T","year":"1994","journal-title":"ACM Trans Comput Syst"},{"key":"p_37","first-page":"178","volume-title":"IEEE computer society symposium on research in security and privacy","author":"Woo TYC","year":"1993"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0058-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0058-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0058-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:44:21Z","timestamp":1641483861000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0058-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,10]]}},"alternative-id":["10.1007\/s00165-004-0058-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0058-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,10]]}}}