Abstract. Web services security specifications are typically expressed as a mixture of XML schemas, example messages, and narrative explanations. We propose a new specification language for writing complementary machine-checkable descriptions of SOAP-based security protocols and their properties. Our TulaFale language is based on the pi calculus (for writing collections of SOAP processors running in parallel), plus XML syntax (to express SOAP messaging), logical predicates (to construct and filter SOAP messages), and correspondence assertions (to specify authentication goals of protocols). Our implementation compiles TulaFale into the applied pi calculus, and then runs Blanchet's resolution-based protocol verifier. Hence, we can automatically verify authentication properties of SOAP protocols. Web services are a wide-area distributed systems technology, based on asynchronous exchanges of XML messages conforming to the SOAP message format [BEK + 00,W3C03]. The WS-Security standard [NKHBM04] describes how to sign and encrypt portions of SOAP messages, so as to achieve end-to-end security. This paper introduces TulaFale, a new language for defining and automatically verifying models of SOAP-based cryptographic protocols, and illustrates its usage for a typical request/response protocol: we sketch the protocol, describe potential attacks, and then give a detailed description of how to define and check the request and response messages in TulaFale. A basic motivation for web services is to support programmatic access to web data. The HTML returned by a typical website is a mixture of data and presentational markup, well suited for human browsing, but the presence of markup makes HTML a messy and brittle format for data processing. In contrast, the XML returned by a web service is just the data, with some clearly distinguished metadata, well suited for programmatic access. For example, search engines export web services for programmatic web search, and e-commerce sites export web services to allow affiliated websites direct access to their databases. Generally, a broad range of applications for web services is emerging, from the well-established use of SOAP as a platform and vendor neutral middleware within a single organisation, to the proposed use of SOAP for device-to-device interaction [S + 04]. In the beginning, "SOAP" stood for "Simple Object Access Protocol", and was intended to implement "RPC using XML over HTTP" [Win98, Win99, Box01] . HTTP facilitates interoperability between geographically distant machines and between those in protection domains separated by corporate firewalls that block many other transports. XML facilitates interoperability between different suppliers' implementations, unlike various binary formats of previous RPC technologies. Still, web services technology should not be misconstrued as HTTP-specific RPC for distributed objects [Vog03] . HTTP is certainly at present the most common transport protocol, but the SOAP format is independent of HTTP, and some web services use other transports such as TCP or SMTP [SMWC03] . The design goals of SOAP/1.1 [BEK + 00] explicitly preclude object-oriented features such as object activation and distributed garbage collection; by version 1.2 [W3C03], "SOAP" is a pure name, not an acronym. The primitive message pattern in SOAP is a single one-way message that may be processed by zero or more intermediaries between two end-points; RPC is a derived message pattern built from a request and a response. In brief, SOAP is not tied to objects, and web services are not tied to the web. Still, our running example is an RPC over HTTP, which still appears to be the common case. Web services specifications support SOAP-level security via a syntax for embedding cryptographic materials in SOAP messages. To meet their security goals, web services and their clients can construct and check security headers in messages, according to the WS-Security format [IM02, NKHBM04] . WS-Security can provide message confidentiality and authentication independently of the underlying transport, using, for instance, secure hash functions, shared-key encryption, or public-key cryptography. WS-Security has several advantages compared to using a secure transport such as SSL, including scalability, flexibility, transparency to intermediaries such as firewalls, and support for non-repudiation. Significantly, though, WS-Security does not itself prescribe a particular security protocol: each application must determine its security goals, and process security headers accordingly. Web services may be vulnerable to many of the well-documented classes of attack on ordinary websites [SS02,HL03]. Moreover, unlike typical websites, web services relying on SOAP-based cryptographic protocols may additionally be vulnerable to a new class of XML rewriting attacks: a range of attacks in which an attacker may record, modify, replay, and redirect SOAP messages, but without breaking the underlying cryptographic algorithms. Flexibility comes at a price in terms of security, and it is surprisingly easy to misinterpret the guarantees actually obtained from processing security headers. XML is hence a new setting for an old problem going back to Needham and Schroeder's pioneering work on authentication protocols; SOAP security protocols should be judged safe, or not, with respect to an attacker who is able to "interpose a computer on 2 all communication paths, and thus can alter or copy parts of messages, replay messages, or emit false material" [NS78] . XML rewriting attacks are included in the WS-I threat model [DHK + 04]. We have found a variety of replay and impersonation attacks in practice. The use of formal methods to analyze cryptographic protocols and their vulnerabilities begin with work by Dolev and Yao [DY83]. In the past few years there has been intense research on the Dolev-Yao model, leading to the development of numerous formalisms and tools. TulaFale builds on the line of research using the pi calculus. The pi calculus [Mil99] is a general theory of interaction between concurrent processes. Several variants of the pi calculus, including spi [AG99], and a generalization, applied pi [AF01], have been used to formalize and prove properties of cryptographic protocols. A range of compositional reasoning techniques is available for proving protocol properties, but proofs typically require human skill and determination. Recently, however, Blanchet [Bla01, Bla02] has proposed a range of automatic techniques, embodied in his theorem prover ProVerif, for checking certain secrecy and authentication properties of the applied pi calculus. ProVerif works by compiling the pi calculus to Horn clauses and then running resolutionbased algorithms. TulaFale is a new scripting language for specifying SOAP security protocols, and verifying the absence of XML rewriting attacks: TulaFale = processes + XML + predicates + assertions The pi calculus is the core of TulaFale, and allows us to describe SOAP processors, such as clients and servers, as communicating processes. We extend the pi calculus with a syntax for XML plus symbolic cryptographic operations; hence, we can directly express SOAP messaging with WS-Security headers. We declaratively specify the construction and checking of SOAP messages using Prolog-style predicates; hence, we can describe the operational details of SOAP processing. Independently, we specify security goals using various assertions, such as correspondences for message authentication and correlation. It is important that TulaFale can express the detailed structure of XML signatures and encryption so as to catch low-level attacks on this structure, such as copying part of an XML signature into another; more abstract representations of message formats, typical in the study of the Dolev-Yao model and used for instance in previous work on SOAP authentication protocols [GP03] , are insensitive to such attacks. Our methodology when developing TulaFale has been to study particular web services implementations, and to develop TulaFale scripts modelling their , a particular implementation of WS-Security and related specifications. We have implemented the running example protocol of this paper using WSE, and checked that the SOAP messages specified in our script faithfully reflect the SOAP messages observed in this implementation. For a discussion of the implementation of related protocols, including logs of SOAP messages, see the technical report version of an earlier paper [BFG04a] . Fig. 1 illustrates our methodology. On the left, we have the user-supplied code for implementing a web services protocol, such as the one of this paper, on top of the WSE library. On the right, we have the TulaFale script modelling the user-supplied code, together with some library predicates modelling operations performed by WSE. Also on the right, we have the TulaFale tool, which compiles its input scripts into the pure applied pi calculus to be analyzed via ProVerif. TulaFale is a direct implementation of the pi calculus described in a previous formal semantics of web services authentication [BFG04a] . The original contribution of this paper is to present a concrete language design, to report an implementation of automatic verification of assertions in TulaFale scripts using Blanchet's ProVerif, and to develop a substantial example. Section 2 informally introduces a simple request/response protocol and its security goals: authentication and correlation of the two messages. Section 3 presents TulaFale syntax for XML with symbolic cryptography and for predicates, and as a source of examples, explains a library of TulaFale predicates for constructing and checking SOAP messages. Section 4 describes predicates specific to the messages of our request/response protocol. Section 5 introduces processes and security assertions in TulaFale, and outlines their implementation via ProVerif. Section 6 describes processes and predicates specific to our protocol, and shows how to verify its security goals. Finally, Section 7 concludes. We consider a simple SOAP-based request/response protocol, of the kind easily implemented using WSE to make an RPC to a web service. Our security goals are simply message authentication and correlation. To achieve these goals, the request includes a username token identifying a particular user and a signature token signed by a key derived from user's password; conversely, the response includes a signature token signed by the server's public key. Moreover, to preserve the confidentiality of the user's password from dictionary attacks, the username token in the request message is encrypted with the server's public key. (For simplicity, we are not concerned here with any secrecy properties, such as confidentiality of the actual message bodies, and we do not model any authorization policies.) In the remainder of this section, we present a detailed but informal specification of our intended protocol, and consider some variations subject to XML rewriting attacks. Our protocol involves the following principals: -A single certification authority (CA) issuing X.509 public-key certificates for services, signed with the CA's private key. -Two servers, each equipped with a public key certified by the CA and exporting an arbitrary number of web services. -Multiple clients, acting on behalf of human users. Trust between principals is modelled as a database associating passwords to authorized user names, accessible from clients and servers. Our threat model features an active attacker in control of the network, in possession of all public keys and user names, but not in possession of any of the following: (1) The private key of the CA. (2) The private key of any public key certified by the CA. (3) The password of any user in the database. The second and third points essentially rule out "insider attacks"; we are assuming that the clients, servers, and CA belong to a single close-knit institution. It is easy to extend our model to study the impact of insider attacks, and indeed to allow more than two servers, but we omit the details in this expository example. Fig. 2 shows an intended run of the protocol between a client and server. -The principal Client(kr,U) acts on behalf of a user identified by U (an XML encoding of the username and password). The parameter kr is the public key of the CA, needed by the client to check the validity of public key certificates. -The principal Server(sx,cert,S) implements a service identified by S (an XML encoding of a URL address, a SOAP action, and the subject name appearing on the service's certificate). The parameter sx is the server's private signing key, while cert is its public certificate. -The client sends a request message satisfying isMsg1(−,U,S,id1,t1,b1), which we define later to mean the message has body b1, timestamp t1, and message identifier id1, is addressed to a web service S, and has a <Security> header containing a token identifying U and encrypted with S's public key, and a signature of S, id1, t1, and b1 by U. -The server sends a response message satisfying isMsg2(−,S,id1,id2,t2,b2), which we define later to mean the message has body b2, timestamp t2, and message identifier id2, is sent from S, and has a <Security> header containing S's certificate cert and a signature of id1, id2, t2, and b2 by S. -The client and server enact begin-and end-events labelled C1(U,S,id1,t1,b1) to record the data agreed after receipt of the first message. Similarly, the begin-and end-events labelled C2(U,S,id1,t1,b1,id2,t2,b2) record the data agreed after both messages are received. Each begin-event marks an intention to send data. Each end-event marks apparently successful agreement on data. The begin-and end-events define our authentication and correlation goals: for every end-event with a particular label, there is a preceding begin-event with the same label in any run of the system, even in the presence of an active attacker. Such goals are known as one-to-many correspondences [WL93] or non-injective agreements [Low97] . The C1 events specify authentication of the request, while the C2 events specify authentication of the response. By including data from the request, C2 events also specify correlation of the request and response. Like most message sequence notations, Fig. 2 simply illustrates a typical protocol run, and is not in itself an adequate specification. In Sections 4 and 6 we present a formal specification in TulaFale: we define the principals Client(kr,U) and Server(sx,cert,S) as parametric processes, and we define the checks isMsg1 and isMsg2 as predicates on our model of XML with symbolic cryptography. The formal model clarifies the following points, which are left implicit in the figure: -The client can arbitrarily choose which service S to call, and which data t1 and b1 to send. (In the formal model, we typically make such arbitrary choices by inputting the data from the opponent.) Conversely, the client must generate a fresh identifier id1 for each request, or else it is impossible to correlate the responses from two simultaneous requests to the same service. -Similarly, the server can arbitrarily choose the response data id2, t2, and b2. On the other hand, our formal model does not directly address replay protection. To rule out direct replays of correctly signed messages, we would need to specify that for each end-event there is a unique preceding begin-event with the same label. This is known as a one-to-one correspondence or injective agreement. In practice, we can protect against direct replays using a cache of recently received message identifiers and timestamps to ensure that no two messages are accepted with the same identifier and timestamp. Hence, if we can prove that the protocol establishes non-injective agreement on data including the identifiers and timestamps, then, given such replay protection, the protocol implementation also establishes injective agreement. We end this section by discussing some flawed variations of the protocol, corresponding to actual flaws we have encountered in user code for web services. -Suppose that the check isMsg1(−,U,S,id1,t1,b1) only requires that S, id1, and b1, are signed by U, but not the timestamp t1. Replay protection based on the timestamp is now ineffective: the opponent can record a message with timestamp t1, wait until some time t2 when the timestamp has expired, and the message identifier id1 is no longer being cached, rewrite the original message with timestamp t2, and then replay the message. The resulting message satisfies isMsg1(−,U,S,id1,t2,b1), since t2 does not need to be signed, and hence is accepted by the server. Fig. 3 shows the attack, and the resulting failure of correspondence C1. -Suppose that a client re-uses the same message identifier in two different calls to a web service; the opponent can manipulate messages so that the client treats the response to the first call as if it were the response to the second call. Fig. 4 shows the attack. The client sends a first request with body b1 and identifier id1. The opponent intercepts the response with body b2, and sends a SOAP fault back to the client. Subsequently, the client sends a second request with the same identifier id1 as the first, and body b1'. The opponent can delete this request to prevent it reaching the service, and then replay the original response. The client now considers that b2 is the response to b1', when in fact it is the response to b1, perhaps completely different. Formally, this is a failure of correspondence C2. -Suppose that the server does not include the request identifier id1 in the signature on the response message. Then the opponent can mount a similar correlation attack, breaking C2-we omit the details. We can easily adapt our TulaFale script to model these variations in the protocol. Our tool automatically and swiftly detects the errors, and returns descriptions of the messages sent during the attacks. These flaws in web services code are typical of errors in cryptographic protocols historically. The practical impact of these flaws is hard to assess, as they were found in preliminary code, before deployment. Still, it is prudent to eliminate these vulnerabilities, and tools such as TulaFale can systematically rule them out. This section introduces the term and predicate language of TulaFale, via a series of basic constructions needed for the example protocol of Section 2. Throughout 8 the paper, for the sake of exposition, we elide some details of SOAP envelopes, such as certain headers and attributes, that are unconnected to security. Here is a TulaFale term for a SOAP request, illustrating the format of the first message in our example protocol: Every SOAP message consists of an XML <Envelope> element, with two children: an optional <Header> and a mandatory <Body>. In this example, the header has four children, and the body has an Id-attribute, the literal string "1". We base TulaFale on a sorted (or typed) term algebra, built up from a set of function symbols and variables. The basic sorts for XML data include string (for string literals), att (for named attributes), and item (either an element or a string). Every element or attribute tag (such as Envelope or Id, for example) corresponds to a sorted function symbol in the underlying algebra. Although TulaFale syntax is close to the XML wire format, it is not identical. We suppress all namespace information. As previously mentioned, we omit closing element tags; for example, we write </> instead of </Envelope>. Literal strings are always quoted, as in <Created>"2004-03-19T09:46:32Z"</>. In the standard wire format, the double quotes would be omitted when a string is an element body. We use quotation to distinguish strings from term variables, such as the variables uri, ac, id, utok, sig, and request in the example above. In TulaFale, we represent cryptographic algorithms symbolically, as function symbols that act on a sort bytes of byte arrays. Each function is either a data constructor, with no accompanying rewrite rule, or it is a destructor, equipped with a rewrite rule for testing or extracting data from an application of a constructor. For example, encryption functions are constructors, and decryption functions are destructors. This approach, the basis of the Dolev-Yao model [DY83], assumes 9 that the underlying cryptography is perfect, and can be faithfully reflected by abstract equational properties of the functions. It also abstracts some details, such as the lengths of strings and byte arrays. The TulaFale syntax for introducing constructors and destructors is based on the syntax used by ProVerif. For instance, we declare function symbols for RSA key generation, public-key encryption, and private-key decryption using the following TulaFale declarations: constructor pk(bytes):bytes. constructor rsa(bytes,bytes):bytes. destructor decrsa(bytes,bytes):bytes with decrsa(s,rsa(pk(s),b)) = b. The constructor pk represents the relationship between private and public keys (both byte arrays, of sort bytes); it takes a private key and returns the corresponding public key. There is no inverse or destructor, as we intend to represent a one-way function: given only pk(s) it is impossible to extract s. The constructor rsa(k,x) encrypts the data x:bytes under the public key k, producing an encrypted byte array. The destructor decrsa(s,e) uses the corresponding private key s to decrypt a byte array generated by rsa(pk(s),x). The destructor definition expresses the decryption operation as a rewrite rule: when an application of decrsa in a term matches the left-hand side of the rule, it may be replaced by the corresponding right-hand side. To declare RSA public-key signatures, we introduce another constructor rsasha1(s,x) that produces a RSA signature of a cryptographic hash of data x under the private key s: constructor rsasha1(bytes,bytes):bytes. destructor checkrsasha1(bytes,bytes,bytes):bytes with checkrsasha1(pk(s),x,rsasha1(s,x))=pk(s). To check the validity of a signature sig on x using a public key k, one can form the term checkrsasha1(k,x,sig) and compare it to k. If k is a public key of the form pk(s) and sig is the result of signing x under the corresponding private key s, then this term rewrites to k. For the purposes of this paper, an X.509 certificate binds a key to a subject name by embedding a digital signature generated from the private key of some certifying authority (CA). We declare X.509 certificates as follows: constructor x509(bytes,string,string,bytes):bytes. destructor x509key(bytes):bytes with x509key(x509(s,u,a,k))=k. destructor x509user(bytes):string with x509user(x509(s,u,a,k))=u. destructor x509alg(bytes):string with x509alg(x509(s,u,a,k))=a. destructor checkx509(bytes,bytes):bytes with checkx509(x509(sr,u,a,k),pk(sr))=pk(sr). The term x509(sr,u,a,k) represents a certificate that binds the subject name u to the public key k, for use with the signature algorithm a (typically rsasha1). This certificate is signed by the CA with private key sr. Given such a certificate, the destructors x509key, x509user, and x509alg extract the three public fields of the certificate. Much like checkrsasha1 for ordinary digital signatures, an additional destructor checkx509 can be used to check the authenticity of the embedded signature. Next, we write logical predicates to construct and parse XML encrypted under some known RSA public key. A predicate is written using a Prolog-like syntax; it takes a tuple of terms and checks logical properties, such as whether two terms are equal or whether a term has a specific format. It is useful to think of some of the terms given to the predicate as inputs and the others as outputs. Under this interpretation, the predicate computes output terms that satisfy the logical properties by pattern-matching. The predicate mkEncryptedData takes a plaintext plain:item and an RSA public encryption key ek:bytes, and it generates an XML element encrypted containing the XML encoding of plain encrypted under ek. predicate mkEncryptedData (encrypted:item,plain:item,ek:bytes) :− cipher = rsa(ek,c14n(plain)), encrypted = <EncryptedData> <CipherData> <CipherValue>base64(cipher)</></></>. The first binding in the predicate definition computes the encrypted byte array, cipher, using the rsa encryption function applied to the key ek and the plaintext plain. Since rsa is only defined over byte arrays, plain:item is first converted to bytes using the (reversible) c14n constructor. The second binding generates an XML element (<EncryptedData>) containing the encrypted bytes. Since only strings or elements can be embedded into XML elements, the encrypted byte array, cipher, is first converted to a string using the (reversible) base64 constructor. In this paper, we use three transformation functions between sorts: c14n (with inverse ic14n) transforms an item to a bytes, base64 (with inverse ibase64) transforms a bytes to a string, and utf8 (with inverse iutf8) transforms a string to a bytes. All three functions have specific meanings in the context of XML transformations, but we treat them simply as coercion functions between sorts. To process a given element, <Foo> say, we sometimes write distinct predicates on the sending side and on the receiving side of the protocol, respectively. By convention, to construct a <Foo> element, we write a predicate named mkFoo whose first parameter is the element being constructed; to parse and check it, we write a predicate named isFoo. For <EncryptedData>, for instance, the logical predicate isEncryptedData parses elements constructed by mkEncryptedData; it takes an element encrypted 11 and a decryption key dk:bytes and, if encrypted is an <EncryptedData> element with some plaintext encrypted under the corresponding encryption key pk(dk), it returns the plaintext as plain. predicate isEncryptedData (encrypted:item,plain:item,dk:bytes) :− encrypted = <EncryptedData> <CipherData> <CipherValue>base64(cipher)</></></>, c14n(plain) = decrsa(dk,cipher). Abstractly, this predicate reverses the computations performed by mkEncryptedData. One difference, of course, is that while mkEncryptedData is passed the public encryption key ek, the isEncryptedData predicate is instead passed the private key, dk. The first line matches encrypted against a pattern representing the <EncryptedData> element, extracting the encrypted byte array, cipher. Relying on pattern-matching, the constructor base64 is implicitly inverted using its destructor ibase64. The second line decrypts cipher using the decryption key dk, and implicitly inverts c14n using its destructor ic14n to compute plain. Services and X509 Security Tokens
Karthikeyan Bhargavan et al. REF developed a tool called TulaFale to specify SOAP-based security protocols in pi-calculus and analyze its vulnerabilities.
TulaFale: A Security Tool for Web Services
ArXiv
ArXiv
Computer Science