Most works that extend workflow validation beyond syn- tactical checking consider constraints on the sequence of messages exchanged between services. However, these con- straints are expressed only in terms of message names and abstract away their actual data content. Using the context of the User-controlled Lightpath initiative (UCLP) hosted by the CANARIE consortium, we provide examples of real- world "data-aware" web service constraints where the se- quence of messages and their content are interdependent. We present CTL-FO+, an extension over Computation Tree Logic that includes first-order quantification on state vari- ables in addition to temporal operators. We show how CTL- FO+ is adequate for expressing data-aware constraints, give a complete model checking algorithm for CTL-FO+ and establish its complexity to be PSPACE-complete. This makes using CTL-FO+ for validating workflow properties no harder than using the Linear Temporal Logic (LTL) al- ready used by some web service tools. Finally, we show how the modelling of data-aware properties is an increase in ex- pressiveness that cannot be efficiently simulated by these tools.