Validating a Web Service Security Abstraction by Typing

Abstraction by Typing Andrew D. Gordon Microsoft Research Riccardo Pucella Cornell University 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 appe...

• Type: Journal
• Year: 2004
• Where: CORR
• Authors: Andrew D. Gordon, Riccardo Pucella
• Keywords: CORR 2004, Education, Research Riccardo Pucella, Security, University An XML