Workflow provides a promising solution for organizations to achieve their business goals by interactions and collaborations between Web services. Access control is an important security mechanism to protect the resources to be only accessed by authorized users in such collaborative environments. In this paper, we aim at developing a method for formalizing and analyzing workflow access control in Web service context. To achieve this goal, we first present WSPI, Web Service Pi calculus, to formalize Web services and workflow processes. Based on WSPI, a type system is proposed to ensure that the specified TBAC policy is respected during system reductions. By subject reduction, the well-typed system can guarantee the system security and avoid access violations in run time.