A requirements analysis in the emerging field of Semantic Web Services (SWS) (see http://daml.org/services/swsl/requirements/) has identified four major areas of research: intelligent service discovery, automated contracting of services, process modeling, and service enactment. This paper deals with the intersection of two of these areas: process modeling as it pertains to automated contracting. Specifically, we propose a logic, called CT R-S, which captures the dynamic aspects of contracting for services. Since CT R-S is an extension of the classical first-order logic, it is well-suited to model the static aspects of contracting as well. A distinctive feature of contracting is that it involves two or more parties in a potentially adversarial situation. CT R-S is designed to model this adversarial situation through its novel model theory, which incorporates certain game-Theoretic concepts. In addition to the model theory, we develop a proof theory for CT R-S and demonstrate the use of the logic for modeling and reasoning about Web service contracts.