Contemporary open systems use components developed by many different parties,
linked together dynamically in unforeseen constellations. Code needs to live up to
strict security specifications: it has to ensure the correct functioning of its
objects when they collaborate with external objects which may be malicious. In this
paper we propose specifications that model risk and trust in such open systems. We
specify Miller, Van Cutsem, and Tulloh’s escrow exchange example, and discuss the
meaning of such a specification. We argue informally that the code satisfies its
specification.