The example is originally due to Peleska, who argues that, in order 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 a tutorial introduction to the use of mechanized formal state exploration methods (specifically, the Murphi system from Stanford) for the purpose of examining and debugging protocols, and the use of theorem proving and model-checking to verify them.
PDF
@string{csl = {Computer Science Laboratory, SRI International}}
@string{mp = {Menlo Park, CA}}
@techreport{Rushby95:caution,
AUTHOR = {John Rushby},
TITLE = {Combining System Properties: A Cautionary Example and
Formal Examination},
INSTITUTION = csl,
YEAR = 1995,
MONTH = jun,
ADDRESS = mp,
NOTE = {Technical Report; included in the Mur$\phi$
distribution, and also available at \url{http://www.csl.sri.com/~rushby/papers/combined95.pdf}}
}