Validating a Web Service Security Abstraction by Typing

TL;DR

This paper introduces a type-based security abstraction for XML web services that verifies request and response authentication at the SOAP level, enhancing security without relying solely on transport-layer protocols.

Contribution

It models web service security as a typed object calculus, translating it into cryptographic primitives and verifying authentication through type checking, with an implementation using custom SOAP headers.

Findings

Type system verifies authentication correctness

Semantic model ensures security properties

Implementation demonstrates practical feasibility

Abstract

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.