Abstract : This technical report describes the work of the Dependable System Architecture Group on the Secure Distributed Transaction Processing (SDTP) project. Chapter 1 provides an overview of secure software architectures. Chapter 2 describes the goals and methodology of the SDTP project. Chapter 3 of this report provides a proof of the model-theoretic approach used in the project to prove that refinement steps are faithful and preserve both security and faithful properties. Chapter 4 introduces an alternative method of proving refinement. Chapter 5 describes the method for showing patterns are faithful and hence security-preserving. Chapter 6 shows refinement patterns that do not always preserve a property of interest, such as security, can be used without losing the correctness guarantee that a restriction to validated refinement patterns automatically provides. Chapter 7 discusses a case study in architecture verification. Finally, Chapter 8 provides more detail on the reference implementation and describes two applications of the reference implementation (law enforcement and intrusion detection).