Abstract : The objective of this research was to develop mechanisms and methods of analysis to support construction of survivable systems where survivable means systems able to withstand multiple kinds of faults among their components, including those induced deliberately by an active attacker. One class of architectures for survivability builds on classical methods for fault tolerance, in which replication and voting are used to mask faults. An alternative class of methods requires less tight coordination, giving rise to loosely coupled architectures. Mechanisms that support survivability in loosely coupled architectures are typically based on cryptography, and much of the work performed in this project focused on development of suitable cryptographic protocols and on their formal verification. In the course of the project, the state of the art was advanced from one where formal verification of these protocols was a tour de force to one where it may be considered routine and available for general deployment. The outputs of this research are documented in a series of technical papers (with associated abstracts) that follow.