Computer Science – Cryptography and Security
Scientific paper
2004-12-10
Formal Aspects of Computing 17 (3), pp. 277-318, 2005
Computer Science
Cryptography and Security
44 pages. A preliminary version appears in the Proceedings of the Workshop on XML Security 2002, pp. 18-29, November 2002
Scientific paper
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.
Gordon Andrew D.
Pucella Riccardo
No associations
LandOfFree
Validating a Web Service Security Abstraction by Typing does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Validating a Web Service Security Abstraction by Typing, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Validating a Web Service Security Abstraction by Typing will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-263523