Service-oriented architectures (SOAs) enable the dynamic integration of services implemented on heterogeneous computer systems. An advantage of SOAs is that they provide high-level, semantically-rich services by abstracting the low-level details of their implementation. The availability of useful services such as Google's and Amazon's web service APIs has fostered applications that integrate a number of services to provide novel, more complex functionality. As the service-oriented model is increasingly adopted, there is a need for rigorous approaches to model trust in SOAs and ensure trust in the composition of services, in the form of service-based applications. These approaches should guarantee that by composing services that satisfy certain trust properties one will obtain an application that satisfies the desired trust properties. The goal of this project is to develop novel tools and techniques for the modeling and analysis of trust properties of SOA-based applications. More precisely, the goal of this research is to develop a framework that leverages formal models of trust, automated, and interactive verification techniques, and program analysis techniques to address trust properties of single services and of their compositions, at both the interface and implementation levels. The broader impact of this research will be a comprehensive framework that provides a number of techniques and tools for the modeling, analysis, and enforcement of trust properties in SOA-based applications. These tools and techniques will provide a more trustworthy infrastructure for the implementation of SOA-based applications in governmental, military, and private environments.