This report presents a simple example to demonstrate that the composition of a "fault-tolerant" service and a "secure" service does not necessarily provide a secure and fault-tolerant service.

The example is originally due to Peleska, who argues that to achieve the combined service, it is necessary to strengthen one of the individual services to address both concerns. In contrast, I argue that the individual services should be "deconstructed" into smaller and weaker components that can be reassembled in different ways, and I show that the combined service can be achieved by composing the fault-tolerant service with a weaker version of the secure service.

The report also provides an introduction to the use of mechanized formal state exploration methods (specifically, the MurΦ system from Stanford) for the purpose of examining and debugging protocols.

• combined.dvi
• combined.ps